Repository navigation
Proofs is not a gate: paths: proofs/** filter, z3 … || true, Isabelle/Mizar skipped without failing, no assumption check in CI #161
Description
Scope: the Coq/Agda/Z3/Isabelle/Mizar orchestration. The Lean leg (FilesystemCNO/LambdaCNO derive False; never run in CI) is #125; Coq axiom and Idris believe_me debt is #70; the Idris postulates are #27. None of that is duplicated here.
Measured (2026-09-22, main = 74202cb)
.github/workflows/proofs.yml:20–26paths: ['proofs/**']on push and pull_request: a change to the workflow itself, toJustfile, or to any prover config outsideproofs/never runs the proofs. The workflow is absent from the last 12 runs on main.proofs.yml:94sh proofs/z3/verify.sh || true: the Z3 CNO checks cannot fail the job.:95z3 proofs/z3/ond/OND_checks.smt2can, but only by exit code, never by assertingunsat/sattext.proofs/verify-all-provers.sh:41–53: Isabelle and Mizar print "(skipped)" when absent and do not setfail=1, so the script can say green on 4 of 6 provers. Z3, and Isabelle when present, do setfail=1.proofs.yml:80–82type-checks onlyCNO.agdaandOND.agda(the third file,EchoBridgeCNO.agda, isEchoBridgeCNO.agdahas no--safe --without-Kpragma and is not checked by proofs.yml, while PROOF-STATUS:154 says it type-checks under--safe#162).- No
Print Assumptions(Coq) or#print axioms(Lean) step exists anywhere in CI. The Coq side carries 37 liveAxiom/Parameterdeclarations, 13 tagged METAL-BOUNDARY (proof-debt: triage matches proven#107 overly-cautious-OWED pattern — 17 Coq axioms + 5 Idris believe_me's discharge candidates #70 tracks the debt itself); "closed under the global context" is prose until a run prints the list.
Why it matters
A workflow that does not run on the commits that change it, cannot fail on the checks that matter, and never prints its assumptions is a green square with no predicate behind it.
Acceptance criteria
- The
paths:filter is removed, or widened to include.github/workflows/proofs.yml,Justfile,*.agda-lib,_CoqProject,lakefile*, so the workflow runs on every push to main. Watched-failing → green: it appears ingh run list -b mainfor the fix commit. || trueremoved at:94; the Z3 step asserts the expectedunsat/satlines fromverify.shoutput, not just exit 0.verify-all-provers.shsetsfail=1when a prover is absent unless the caller sets an explicitSKIP_ISABELLE=1/SKIP_MIZAR=1; CI sets neither. Mutant: withisabelleoff PATH and no skip variable, the script exits non-zero.- An assumption step:
coqchkplusPrint Assumptions <headline theorem>.for each headline theorem, with the output asserted to list only the METAL-BOUNDARY axioms; the CI log shows the lists. - Ordering per owner ruling D-3 (2026-09-22): Lean FilesystemCNO and LambdaCNO each prove False; lake build reports success and CI never runs the Lean leg #125 is fixed first; this issue's items follow it (Phase 4b–4c of the residual-evidence-types family plan).
🤖 Generated with Claude Code
Activity
hyperpolymath commentedon Sep 22, 2026
Additional consequence measured 2026-09-22T22:46Z while landing #165: because
proofs.ymlis path-filtered toproofs/**,absolute-zero-abi.ipkgand itself, none of its jobs (Coq — CNO + OND (14 theories),Agda — CNO + OND,Z3 — CNO + OND bounded checks) can ever be listed in ruleset 18110203'srequired_status_checks: a PR that touches nothing underproofs/would never report the check, and the rule isstrict_required_status_checks_policy: true, so it would block forever.Proofshas 0 runs onmainamong the last 12 workflow runs.Acceptance criterion to add: the workflow triggers on every
pull_requestandpushtomainwith nopaths:filter; each job decides internally (apaths-filter-freegit diff --name-onlystep or an always-true run) so that it reportssuccesscheaply on non-proof PRs and runs the provers whenproofs/**changed. Only then can the three prover jobs be added as required checks.🤖 Generated with Claude Code
fix: resolve repository issues, port Lean FilesystemCNO, and unify Co…
hyperpolymath commentedon Oct 1, 2026
Status against each criterion on
main(8007381), mostly landed by 877ede2 (#172):on.pushtomainhas nopaths:filter. Thepull_requestfilter includesproofs/**(covers_CoqProject),proofs.yml,Justfile,*.agda-libandlakefile*. Proofs run 36872247986 ran on 8007381.|| trueremains inproofs.yml. The Z3 step reports "every (check-sat) verdict matched its ; expect annotation".proofs/verify-all-provers.shsetsfail=1on every absent prover. Isabelle and Mizar skip only under an explicitSKIP_ISABELLE=1/SKIP_MIZAR=1, and no workflow sets either (grep SKIP_ .github/workflows→ none). The mutant run (isabelle off PATH) was not re-run here.check-assumptions.shgatesPrint Assumptionsfor 17 named theorems and requires each to be Closed under the global context, which is stronger than "lists only METAL-BOUNDARY axioms". It has a--controlthat must rejectlandauer_limit_positive. But nocoqchkstep exists anywhere inproofs/or.github/workflows/. That is the one remaining item.Leaving open for criterion 4 (
coqchk), or for an owner ruling that the Print Assumptions gate supersedes it.🤖 Generated with Claude Code