fix(ci): gate every Idris2 module — the proof checks could not fail (and #51's fix never landed) - #52
Merged
Merged
Conversation
…k dup-forces-omega
Installing Idris2 0.7.0 -- which had never been installed in this estate -- and
actually running `idris2 --check` revealed that Modal.idr HAS NEVER COMPILED:
Error: While processing type of comonadLaw1. Ambiguous elaboration.
Modal.dup b
Prelude.dup b
Error: No type declaration for Modal.comonadLaw1.
Idris2 0.7.0's Prelude exports `dup : a -> (a, a)` ("Function that duplicates its
input"). Every signature in Modal.idr mentioning `dup` failed to elaborate, so
comonadLaw1/comonadLaw2 had no type declarations and were verified by NOTHING --
while the file header, the candidate checklist, and STATE.a2ml all recorded them
as proved, believe_me-free, at 100%.
Pre-existing, not introduced here: origin/main's copy fails identically (same
errors, shifted line numbers).
ROOT CAUSE of the false record: idris2 was never installed. IDRIS2_PREFIX and
PACK_DIR were exported and pack/bin was on PATH, but the pack tree did not exist,
so `idris2 --check` had never once been runnable locally -- and CI gates only
a-sounder-constitution/, not research/. An unrunnable proof gate produces
confident false records.
Fixes:
* `%hide Prelude.dup` in Modal.idr. It now checks clean (exit 0), believe_me-free
-- the comonad laws are proved for the first time since the file was written.
* New DupForcesOmega.idr machine-checks QTT-INTEGRATION.adoc s5 (exit 0):
dupForcesOmega : (r : Multiplicity) -> plus r r = r
-> Either (r = Zero) (r = Many)
dupForcesOmega Zero Refl = Left Refl
dupForcesOmega One Refl impossible
dupForcesOmega Many Refl = Right Refl
The One case is impossible: `plus One One` reduces to Many, so the premise would
need `Refl : Many = One`. That one unwritable clause is the entire defect. The
file also supplies the plus/mult tables Multiplicity never had.
The name clash was never a coincidence: Prelude.dup IS unrestricted duplication,
and at r = omega Box's dup is exactly Prelude.dup up to the MkBox wrapper. The
compiler had been pointing at the defect all along.
SECOND BROKEN PROOF (recorded, not fixed here): research/tropical/TropicalKleene.idr
also fails (exit 1, "Expected a type declaration"). costMatAddZeroL is written
`rewrite h` with no `in`, followed by `exact ...` -- and `exact` is not Idris2 term
syntax at all. That file uses syntax which has never existed in the language, so it
cannot ever have been run. Needs its own PR.
Proof sweep with idris2 0.7.0, recorded in STATE.a2ml maintenance-status:
PASS research/level-candidates/L11-modal-box/Modal.idr (after this fix)
PASS research/level-candidates/L11-modal-box/DupForcesOmega.idr
PASS a-sounder-constitution/formal/Constitution.idr (the CI-gated one)
FAIL research/tropical/TropicalKleene.idr (pre-existing)
Records corrected across MOTIVATION.adoc, README.adoc, SEMANTICS-DECISION.adoc,
QTT-INTEGRATION.adoc and STATE.a2ml (open-failures 0 -> 1). Top next action is now
to extend the Idris2 CI gate to research/, and to audit every other repo in the
estate recording an Idris2 milestone for the same unrunnable-gate failure mode.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
PR #51 was merged 88s after its first commit, so the fix in its second commit (04e37c8) never landed. main therefore carries docs asserting Modal.idr's comonad laws are proved while main's Modal.idr does not compile. Commit 1 of this branch re-ships that orphaned fix verbatim. Investigating why nothing caught it turned up the real defect: this repo's proof checks cannot fail. 1. `just proof-check-idris2` did `exit 0` when idris2 was absent ("SKIP: idris2 not installed"). idris2 WAS absent, so the recipe was green on every machine in the estate -- it reported success *because* nothing could check the proofs. proof-check-all depends on it, so the whole suite was green. 2. The same recipe passed a full path to `idris2 --check`, but Idris2 derives the expected module name from the path. Verified: it called the broken ABI/Compliance.idr OK and the working ABI/Foreign.idr FAIL -- inverted on both discriminating cases. 3. The CI gate installed idris2 correctly but was path-filtered to a-sounder-constitution/formal/ -- created after this same bug shipped there once (#45). A gate scoped to where the bug last happened only prevents the last bug. It walked straight into research/. 4. Upstream: `idris2 --check` EXITS 0 on a missing import while printing "Error: Module X not found" (verified in a clean room against 0.7.0; type errors, parse errors and name mismatches all exit 1). Any gate of the form `idris2 --check X && ok` is unsound, including #45's. What the sweep found, running Idris2 over this repo for the first time: 6 of 13 modules do not compile, and 5 of those 6 are in verification/proofs/ -- a directory named "proofs", of which only 1 of 6 modules compiles. One shared fingerprint: LTE/NonZero/modNatNZ used with no `import Data.Nat` (Prelude in Idris1, Data.Nat in Idris2). Never-compiled Idris1-era code. scripts/check-idris2-proofs.sh is now the single source of truth for CI and the Justfile. A missing toolchain is fatal, never a skip. Each module is checked from its own source root. A verdict requires exit 0 AND no "Error:" in the output. Known-broken modules are quarantined and must KEEP failing -- if one starts passing, the script fails and tells you to promote it, so the list cannot rot. And an .idr absent from the manifest is an error, so new proofs are gated by default rather than by memory. The gate was adversarially tested against all five of its failure modes (unlisted module, absent toolchain, missing-import-exits-0, gated regression, quarantined module passing) -- each correctly turns it red. Commenting out the %hide fix turns it red, so it would have caught the original bug. Corrects the record: PROOF-STATUS.md is NOT stale. It says 0/7 proven, and 5 of the 6 modules behind those obligations do not compile. It tracks verification/proofs/idris2 only, so a-sounder-constitution and L11 landing never made it stale. It was the one status file in this repo telling the truth, and STATE.a2ml accused it of lying. That claim was mine; it is withdrawn. Not fixed here, recorded in STATE.a2ml: verification/proofs/idris2 (own PR); TropicalKleene.idr (own PR); `just validate-state`, which greps for TOML [metadata] in a committed S-expression template leftover that still says (project "rsr-template-repo"), prints INVALID, and exits 0. And the estate: the exit-0 skip is in 22 repos, 20 with real proof files (paint-type 53, proof-burrower 18). All four prover recipes share it, so it is an rsr-template-repo bug. `lean` is installed nowhere, so every `just proof-check-lean4` in the estate is green right now having verified nothing. Fix the template first. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
hyperpolymath
marked this pull request as ready for review
July 17, 2026 06:10
Attempted the verification/proofs/idris2 fix during the CI wait and
reverted it. `import Data.Nat` is necessary but NOT sufficient: it only
unmasks the next layer of errors, which are real.
Types.idr -> .inBounds is not accessible
ABI/Platform.idr -> Undefined name lteRefl
ABI/Layout.idr -> Can't solve constraint: S ?x vs f .fieldAlignment
ABI/Pointers.idr -> .nonNull not accessible, plus a unification failure
ABI/Compliance.idr inherits ABI/Layout's
Types.idr and ABI/Pointers.idr share a design error rather than a typo:
both declare a proof field at quantity 0 -- `{auto 0 inBounds : LTE value
max}` -- and then project it into a value position (`boundedLeMax b =
b.inBounds`). A 0-quantity field is erased and cannot be returned as a
value, so the projection is inaccessible by construction. Fixing it needs
a deliberate decision about the records' quantities.
The estimate "likely one import line each" was mine, was unverified, and
is withdrawn from STATE.a2ml and the manifest notes. Recording the
measured errors instead so the next person starts from fact.
Note the near-miss: the first check of Types.idr looked green because the
output was truncated at head -8 and the exit code read was the pipe's, not
Idris2's. Re-running it through the gate's own verdict logic (exit 0 AND
no ^Error:) showed it still failing. That is the same class of mistake
this whole branch exists to fix.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
hyperpolymath
added a commit
that referenced
this pull request
Jul 17, 2026
…#53) ## What Make main's **Idris2 Proof** gate pass. It is **red on main right now** (run on merge commit `91b16104` = failure). ## Why main went red PR #52 merged the sound *gate* but with a broken *toolchain step*. The workflow's "Build & install Idris2" ran `tar xzf` **inside the checkout**, extracting `Idris2-0.7.0/` — which ships hundreds of `.idr` files under `libs/`, `benchmark/`, `docs/` — into the very tree the gate sweeps. The gate's rule "any `.idr` not in the manifest is an error" then fired on the *compiler's own sources*. Verified from the run-29559473259 log: `FAIL: Idris2 modules present on disk but absent from the MANIFEST → Idris2-0.7.0/libs/base/...`. The gate did exactly what it should. The workflow was polluting the tree it scanned. ## Fix - Build the toolchain in a `mktemp -d` **outside** the checkout, so the only `.idr` the gate sees are this repo's. - Untrack `src/interface/build/ttc/2025081600/**` — committed TTC caches (`build/` is already gitignored; these predate the rule). *Not* the CI cause — a genuine 0.7.0 build stamps ttc version `2023090800` and ignores a `2025081600` cache — but build output never belongs in git. ##⚠️ Do not merge until the Idris2 Proof check on this PR is green This is the fix for a gate that merged red once already (#52), and #51's real fix was likewise orphaned by a fast merge. Please let the check complete. Consider making **Idris2 Proof** a required status check so a red gate can't ride into main again. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
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.
Why this exists
PR #51 was merged 88 seconds after its first commit landed. Its second commit — the one with the actual fix — was pushed ten minutes later, to a branch whose PR was already closed. It never landed.
cf7f211pushed (docs)04e37c8committed (the fix)So
mainright now says "comonad laws proved (believe_me-free)" whilemain'sModal.idrdoes not compile. The docs mademainsound more authoritative while the fix sat on a dead branch. Commit 1 re-ships04e37c8verbatim (tree-identical; verified).Then I asked why nothing caught it, and that turned out to be the real bug.
The real defect: this repo's proof checks cannot fail
just proof-check-idris2didexit 0when idris2 was absentidris2 --checkABI/Compliance.idr→ OK; workingABI/Foreign.idr→ FAILa-sounder-constitution/formal/research/idris2 --checkexits 0 on a missing importidris2 --check X && okis unsound — including #45's own gateHole 4, verified in a clean room against 0.7.0:
They share one shape: a check that cannot fail. That's not a weak check, it's a null check that emits reassuring text — and every status file downstream inherits the false confidence.
What the first-ever full sweep found
6 of 13 modules don't compile. Five are in
verification/proofs/— a directory named proofs, where only 1 of 6 modules compiles.One shared fingerprint:
LTE/NonZero/modNatNZused with noimport Data.Nat. Those were Prelude in Idris1,Data.Natin Idris2. This is never-compiled Idris1-era code, not rot.The fix
scripts/check-idris2-proofs.sh— single source of truth for CI and the Justfile, so local green and CI green mean the same thing:Error:in output (defeats hole 4).idrabsent from the manifest is an error — new proofs are gated by default rather than by memoryThe gate was tested by watching it fail
A gate never observed failing is the bug under investigation, so:
.idrin tree%hidethe fix)Result: 8 gated PASS · 5 quarantined fail as recorded · 13/13 accounted for.
Correcting the record
PROOF-STATUS.mdis NOT stale. It says 0/7 proven — and 5 of the 6 modules behind those obligations don't compile. It tracksverification/proofs/idris2/only, soa-sounder-constitutionand L11 landing never made it stale. It was the one status file in this repo telling the truth, andSTATE.a2mlaccused it of lying. That claim was mine. It's withdrawn.Also softened: "idris2 was never installed in this estate" is too strong — committed
.ttcartefacts show it ran somewhere around Aug 2025.Not fixed here (recorded in
STATE.a2ml)verification/proofs/idris2/— attempted during the CI wait and reverted; it is NOT a typo sweep.import Data.Natis necessary but only unmasks the next layer:Types.idr.inBoundsnot accessibleABI/Platform.idrUndefined name lteReflABI/Layout.idrCan't solve constraint: S ?x vs f .fieldAlignmentABI/Pointers.idr.nonNullnot accessible + unification failureTypes.idrandABI/Pointers.idrshare a design error, not a typo: both declare a proof field at quantity 0 ({auto 0 inBounds : LTE value max}) and then project it into a value position (boundedLeMax b = b.inBounds). A 0-quantity field is erased and cannot be returned as a value — inaccessible by construction. Needs a deliberate decision about the records' quantities. My earlier estimate "one import line each" was unverified and is withdrawn (commit884389c).Near-miss worth recording: the first check of
Types.idrlooked green because output was truncated athead -8and the exit code read was the pipe's, not Idris2's. Re-run through this branch's own verdict logic (exit 0 and no^Error:), it still failed — the same class of mistake this branch exists to fix.TropicalKleene.idr(own PR)just validate-statehas never validated this project: it greps for TOML[metadata]in a committed S-expression template leftover that still says(project "rsr-template-repo"), printsINVALID, and exits 0The
exit 0skip is rsr-template-repo's, in 22 repos — 20 with real proof files (paint-type 53, ideas-to-alphas 31, proof-burrower 18, snifs 15). All four prover recipes share it (idris2/lean4/agda/coq).Live right now:
leanis installed nowhere, so everyjust proof-check-lean4in the estate is green having verified nothing.Fix the template first, or it re-seeds. Detection:
grep -rlE 'SKIP:.*not installed' */Justfile🤖 Generated with Claude Code