Report the failure exit code under --quiet - #4771
Open
ivmat wants to merge 2 commits into
Open
Conversation
`--quiet`'s help text promises "no output, just an exit code and requested artifacts", but `print_final_summary` returned early under `--quiet` before reaching the `exit(1)` that reports failures, so a failing verification run exited 0. Nothing else set the failure exit code. Suppress only the summary output under `--quiet`: compute the failure counts unconditionally and keep the exit code and error returns identical to a non-quiet run. `print_autoharness_summary` takes a `quiet` flag so it still reports its failure count without printing the summary; this also fixes the same bug for `autoharness --quiet`, whose failure count previously never reached the exit code. Add a regression test that runs a failing harness under `--quiet` and asserts exit 1, plus a passing-run control asserting exit 0 -- the existing check-quiet test only ran passing harnesses and never inspected the exit code. Resolves model-checking#4745
ivmat
force-pushed
the
fix-quiet-exit-code
branch
from
August 27, 2026 20:56
0d20f68 to
7644203
Compare
Contributor
Author
|
earlier CI red was kani-fmt --check wanting a println! collapsed |
celinval
reviewed
Aug 27, 2026
celinval
left a comment
celinval
left a comment
Contributor
There was a problem hiding this comment.
That's a good catch. Thanks for taking the time.
|
|
||
| let autoharness_failing = if self.autoharness_compiler_flags.is_some() { | ||
| self.print_autoharness_summary(automatic)? | ||
| self.print_autoharness_summary(automatic, quiet)? |
Contributor
There was a problem hiding this comment.
I'd prefer if we split print_autoharness_summary. Something like:
// You can move the self.autoharness_compiler_flags.is_some() check to be inside self.autoharness_result.
let autoharness_result = self.autoharness_result(automatic);
if !quiet {
self.print_autoharness_summary(autoharness_result);
}
if failing + autoharness_result.failing.len() {
...
}
Contributor
Author
There was a problem hiding this comment.
done (all), also ran tests locally on linux
Contributor
Author
There was a problem hiding this comment.
dont have same setup locally so missed the clippy test... will fix
| pub fn print_autoharness_summary( | ||
| &self, | ||
| mut automatic: Vec<&HarnessResult<'_>>, | ||
| quiet: bool, |
Contributor
There was a problem hiding this comment.
I know that's not on you, but I think we should change this function should either return Result<()> or nothing, depends whether it fallible or not. It's a print function, it shouldn't really be returning any data.
| if self.args.common_args.quiet { | ||
| return Ok(()); | ||
| } | ||
| // `--quiet` promises "no output, just an exit code and requested artifacts". It must |
Contributor
There was a problem hiding this comment.
nit: I don't think we need this comment.
Address review: separate the compute (partition into successes/failing, now behind an autoharness_result() that folds in the autoharness_compiler_flags.is_some() check) from the print (print_autoharness_summary, now a pure void function with no quiet param and no returned count). print_final_summary computes the autoharness result unconditionally and gates only the print on !quiet, then derives the exit code from failing + the computed failing count, unchanged from before. Also drops the now-superfluous comment block above print_final_summary.
ivmat
force-pushed
the
fix-quiet-exit-code
branch
from
August 28, 2026 16:56
acf1c4e to
0b39b0b
Compare
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Resolves #4745.
--quiet's help text promises "Produces no output, just an exit code and requested artifacts", butprint_final_summaryreturned early under--quietbefore reaching theexit(1)that reports failures, so a failing verification run exited 0. Nothing else set the failure exit code.This suppresses only the summary output under
--quiet: the failure counts are computed unconditionally and the exit code and error returns are kept identical to a non-quiet run.print_autoharness_summarytakes aquietflag so it still reports its failure count without printing — so this also fixes the same swallowed-exit-code bug forautoharness --quiet.Behavior under
--quiet, before → afterautoharnessrun: exit 0 → exit 1 (same root cause).--harnessfilter on a filter-skipping path: this now returns theno_harness_match_error(one line to stdout, exit non-zero) under--quietas well, matching every other hard-error path — which already print and exit non-zero regardless of--quiet. Previously--quietswallowed it into exit 0. (The common zero-match case is already handled earlier bydetermine_targetssince Fail a zero-match harness filter before codegen and export #4743; this only affects the filter-skipping arm.)Test
Extends
tests/script-based-pre/check-quiet: it now runs a failing harness under--quietand asserts exit 1, plus a passing-run control asserting exit 0. The previous test only ran passing harnesses and never inspected the exit code. The check captures both stdout and stderr, since the--quietcontract covers all output, not just stdout.