docs(ci): document rocq-proofs gating rationale + plan (refs #169)#170
Open
avrabe wants to merge 1 commit into
Open
docs(ci): document rocq-proofs gating rationale + plan (refs #169)#170avrabe wants to merge 1 commit into
avrabe wants to merge 1 commit into
Conversation
…plan (#169) #169 asks (correctly) that the rocq-proofs job be gating, not continue-on-error, so a proof regression blocks merge. It can't be made gating right now: the job is currently RED on main due to the upstream rules_rocq_rust toolchain breakage (fixes in flight, #141/#139), so removing continue-on-error would block every merge. The proofs also carry 10 Admitted + 19 Axiom, so criterion 3 ("complete") is separate work. The issue explicitly says a deviation should be documented if there's a reason — there is one, so this documents it inline with the explicit plan to close #169: 1. land the rules_rocq_rust bump (#141/#139) → job green; 2. remove continue-on-error → gating; 3. discharge the Admitted/Axiom separately. Comment-only change; no behavior change. Does NOT remove continue-on-error (would be destructive while the job is red). Refs #169.
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.
Addresses #169 (make rocq-proofs gating) — the part that's safe to do now.
Why not just remove
continue-on-error?The
rocq-proofsjob is currently red on main: it runsbazel build/test //proofs/...and fails on the upstream rules_rocq_rust toolchain breakage (fixes in flight: #141 / #139). Removingcontinue-on-errorwhile red would turn the whole CI gate red and block every merge. So the naive fix is destructive.The proofs also carry 10
Admitted+ 19Axiom, so the issue's criterion 3 ("complete — no axioms standing in for proofs") is separate, larger work.What this does
The issue says a deviation should be documented if there's a reason. There is — so this documents it inline on the job, with the explicit ordered plan to actually close #169:
continue-on-error→ gating;Admitted/Axiomseparately.Comment-only; no behavior change; does not remove
continue-on-error.Refs #169. (Also: #141 and #139 are redundant — both bump rules_rocq_rust — one should be picked to unblock step 1.)
🤖 Generated with Claude Code