From 8cc4ae06fefd140e434541f7f2a189cc8b5eca9f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 6 Jun 2026 08:58:35 +0200 Subject: [PATCH] docs(ci): document why rocq-proofs is continue-on-error + the gating plan (#169) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #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. --- .github/workflows/ci.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 269ed98..6d8e800 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -363,6 +363,15 @@ jobs: # Stays on ubuntu-latest: requires Nix + Bazel; both are out-of-scope for # smithy phase 1 (see migration playbook "What's currently out of scope"). runs-on: ubuntu-latest + # continue-on-error is TEMPORARY, not the intended end state (loom#169). + # The job is currently red because of the upstream rules_rocq_rust toolchain + # breakage (fixes in flight: #141 / #139 bump rules_rocq_rust). Making it + # gating while red would block every merge. Plan to close loom#169: + # 1. land the rules_rocq_rust bump (#141/#139) so this job goes green; + # 2. then REMOVE continue-on-error so a proof regression blocks merge; + # 3. separately discharge the proofs' remaining Admitted/Axiom (criterion + # 3 "complete") — gating catches regressions in the proven parts but + # does not by itself close those gaps. continue-on-error: true steps: - uses: actions/checkout@v4