Emit a warning when Miri is used with optimizations #2814
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Should we also tell the user that this will not significantly improve the performance of running miri except in microbenchmarks? |
RalfJung
reviewed
Mar 17, 2023
| @@ -43,7 +43,7 @@ function run_tests { | |||
| # optimizations up all the way, too). | |||
| # Optimizations change diagnostics (mostly backtraces), so we don't check | |||
| # them. Also error locations change so we don't run the failing tests. | |||
| MIRIFLAGS="${MIRIFLAGS:-} -O -Zmir-opt-level=4" MIRI_SKIP_UI_CHECKS=1 ./miri test -- tests/{pass,panic} | |||
| MIRIFLAGS="${MIRIFLAGS:-} -O -Zmir-opt-level=4 -Cdebug-assertions=yes" MIRI_SKIP_UI_CHECKS=1 ./miri test -- tests/{pass,panic} | |||
There was a problem hiding this comment.
Why add the flag back here? I guess some tests rely on it? Please add a comment.
There was a problem hiding this comment.
Yeah. I considered doing something more clever, such cfg(not(debug_assertions)) on the test cases, but the tests pretty explicitly call debug_assert! so it seemed very circular.
RalfJung
reviewed
Mar 17, 2023
saethlin
force-pushed
the
warn-on-optimization
branch
from
e0863ef to
a67fa85
Compare
RalfJung
reviewed
Mar 18, 2023
|
@bors r+ |
|
☀️ Test successful - checks-actions |
1 similar comment
|
☀️ Test successful - checks-actions |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This may address #2797, by clarifying to the user what is going on and what the consequences of their choices are.
Fixes #2797