Context
rsr-template-repo PR #147 is merged — the canonical honest proof-gate: missing toolchain is FATAL (never a skip), every module is checked from its own source root, the verdict requires exit 0 and no error line, a proof absent from the per-prover MANIFEST is an error, and scan-dangerous.sh is comment-aware.
ideas-to-alphas still ships the SKIP anti-pattern in its Justfile (command -v <prover> || { echo SKIP; exit 0; }) — a gate that cannot fail: it reports green when the prover is absent, e.g. in CI where the prover may not be installed even though it is on the maintainer's box.
This repo is the estate's divergent case — real proofs (~31 files) scattered across a-sounder-constitution/, src/, research/, and verification/proofs/. Piloting here first deliberately de-risks the hard layout before the estate-wide sweep (rsr-template-repo tracking issue).
Do
Acceptance
just proof-check-all fails when a prover is hidden from PATH (verify with a PATH-mask test).- Every real proof is either gated-and-green or honestly quarantined with a real reason.
- No
SKIP: ... not installed remains in any .just/Justfile.
Filed as session wrap-up; pilot not yet started (orientation only).
Context
rsr-template-repo PR #147 is merged — the canonical honest proof-gate: missing toolchain is FATAL (never a skip), every module is checked from its own source root, the verdict requires exit 0 and no error line, a proof absent from the per-prover
MANIFESTis an error, andscan-dangerous.shis comment-aware.ideas-to-alphasstill ships the SKIP anti-pattern in itsJustfile(command -v <prover> || { echo SKIP; exit 0; }) — a gate that cannot fail: it reports green when the prover is absent, e.g. in CI where the prover may not be installed even though it is on the maintainer's box.This repo is the estate's divergent case — real proofs (~31 files) scattered across
a-sounder-constitution/,src/,research/, andverification/proofs/. Piloting here first deliberately de-risks the hard layout before the estate-wide sweep (rsr-template-repo tracking issue).Do
origin/HEAD=main; the working checkout was onfeat/silo; the known-good (but hardcoded) script lives on a third branchfix/idris2-gate-build-outside-checkout(commit6028b95). Reconcile before committing work to any one branch.l11-qtt-integrationworktree is not a live parallel session before touching shared files.scripts/check-proofs.sh <prover>+ per-proververification/proofs/<prover>/MANIFEST+scripts/scan-dangerous.sh) — not the old hardcodedcheck-idris2-proofs.sh.MANIFESTground-truthed by running the provers: idris2 0.7.0 (tools/opt/pack), lean v4.15.0 (tools/opt/elan, off-PATH, via elan), agda 2.6.4.3, coq 8.20.1.proof-check-allintojust ci. Open a signed draft PR.Acceptance
just proof-check-allfails when a prover is hidden from PATH (verify with a PATH-mask test).SKIP: ... not installedremains in any.just/Justfile.Filed as session wrap-up; pilot not yet started (orientation only).