ci(coq): report all thirteen files instead of stopping at the first error - #3342
Open
gHashTag wants to merge 1 commit into
Open
ci(coq): report all thirteen files instead of stopping at the first error#3342gHashTag wants to merge 1 commit into
gHashTag wants to merge 1 commit into
Conversation
…rror Refs #3328 `coqc ... || exit 1` thirteen times stops at the first failure. One CI run therefore yields exactly one error, and finding out how many of the 13 files compile costs one run per file at roughly four minutes each. That was harmless while the job could not start at all. It became the binding constraint the moment it could: this workflow had never got past `opam install`, so coqc had never run on these proofs, and the first thing it said was that file 1 of 13 does not compile. The state of the other twelve was UNKNOWN -- not passing -- and a stop-at-first-error loop cannot answer that question cheaply or at all. The step now attempts every file and prints a table with a count. Failures after the first are tagged FAIL*, because these compile in dependency order and a missing .vo cascades: only the first failure is certainly its own defect. The full coqc output for each failing file goes into a collapsed `::group::` so the table stays readable and nothing is lost. Exit behaviour is unchanged -- any failure still fails the job. Controls, run locally against a stub `coqc`: - stub fails on files 1 and 5 -> "11 of 13 compiled", FAIL on CorePhi.v, FAIL* on Bounds_Mixing.v, exit 1 - stub passes everything -> "All files compiled successfully!", exit 0 Checked with `sh -n` as well as `bash -n`: the container runs `sh -e {0}`, so a bashism would have been a runtime failure and not a syntax error here.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Sep 8, 2026
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
1 participant
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.
Refs #3328
coqc ... || exit 1thirteen times stops at the first failure. One CI runtherefore yields exactly one error, and learning how many of the 13 files
compile costs one run per file at ~4 minutes each.
That was harmless while the job could not start at all. It became the binding
constraint the moment it could: this workflow had never got past
opam install(#3324, #3326), so coqc had never run on these proofs, and the first thing it
said was that file 1 of 13 does not compile. The state of the other twelve is
unknown, not passing — and a stop-at-first-error loop cannot answer that.
What it prints now
These compile in dependency order and a missing
.vocascades, so presentingevery failure as its own defect would overstate the problem. Full
coqcoutputper failing file goes into a collapsed
::group::— nothing is lost, the tablestays readable.
Exit behaviour is unchanged: any failure still fails the job.
Verification
Run locally against a stub
coqc:FAILthenFAIL*, exit 1Checked with
sh -nas well asbash -n— the container runssh -e {0}, so abashism would have been a runtime failure rather than a syntax error.
This PR runs the workflow on itself, so its own run is the first full reading of
how many of the 13 proof files actually compile.