Skip to content

Commit 299344a

Browse files
ci(live-provers): drop continue-on-error on Tier-2/3 live-test steps (#118)
## Summary The two "Run live test for \${{ matrix.backend }} (allow-fail while Wave-X wires up)" steps in `.github/workflows/live-provers.yml` carried `continue-on-error: true`. The comments explicitly disclosed the soft-fail as transitional, but the gate silently masks real prover regressions: a successful Tier-2 / Tier-3 matrix run reports PASS even when the `cargo test` step crashed with a real prover error. This is the same anti-pattern class as echo-types' N5Falsifier xfail gate (resolved via echo-types#136): a self-decaying CI assertion that masks proof-validity once the underlying state matures. ## Scope - Removed `continue-on-error: true` from the Tier-2 live-test step (line 280). - Removed `continue-on-error: true` from the Tier-3 live-test step (line 403). - Renamed both steps to drop the "(allow-fail while Wave-X wires up)" qualifier. ## What is NOT changed Intentional environment resilience preserved: - Job-level `continue-on-error` on tier1-guix / tier3 / tier4 / tier4-gpu (best-effort prover installations). - Step-level `continue-on-error` on "Provision \${{ matrix.backend }}" steps (apt installation of 30+ heterogeneous provers is genuinely best-effort). - Step-level `continue-on-error` on the Tier-4-GPU "Run live version check (SKIP if binary absent)" step (version check is best-effort by design). ## Verification YAML lints clean. No Agda/Coq/Lean files touched — this is a CI-policy change only. ## Refs Estate prover-CI hygiene audit, recorded at: \`standards/adoption-readiness-grades/AUDIT-FINDINGS-2026-05-28.adoc\`. ## Test plan - [ ] CI runs on this PR (will fail-fast on real prover errors instead of silently masking). - [ ] After merge, observe Tier-2/Tier-3 scheduled runs to confirm honest pass/fail signal. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 0aaf866 commit 299344a

1 file changed

Lines changed: 2 additions & 4 deletions

File tree

.github/workflows/live-provers.yml

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -276,8 +276,7 @@ jobs:
276276
hol-light) true ;;
277277
*) "${{ matrix.backend }}" --version 2>/dev/null || true ;;
278278
esac
279-
- name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-2 wires up)
280-
continue-on-error: true
279+
- name: Run live test for ${{ matrix.backend }}
281280
run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
282281

283282
# ============================================================================
@@ -399,8 +398,7 @@ jobs:
399398
ortools) ortools_solve --help 2>&1 | head -n 1 || true ;;
400399
hol4|acl2|scip|imandra) true ;;
401400
esac
402-
- name: Run live test for ${{ matrix.backend }} (allow-fail while Wave-3 wires up)
403-
continue-on-error: true
401+
- name: Run live test for ${{ matrix.backend }}
404402
run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
405403

406404
# ============================================================================

0 commit comments

Comments
 (0)