[hyperpolymath]

What

Moves the proof gate from Agda 2.7.0.1 + a vendored agda-stdlib 3.0-dev SHA to the estate standard: Debian 13's agda-bin=2.6.4.3-1+b2 and agda-stdlib=2.1-4 inside the digest-pinned debian:13-slim image, the same recipe as MetaManifold-Evidence and residual-evidence-types.

Rebased onto #2 (320513d, merged 2026-10-02T14:52Z). #2 brought BenjaminiHochberg/StepUp.agda and the 18-control gate self-test; this PR keeps both as they are on main and re-applies only the toolchain change on top. The two files that conflicted (proofs/PROOF-STATUS.md, proofs/tests/gate-selftest.sh) were resolved by taking main's version and re-applying the toolchain edits; README.md merged cleanly.

Measured

• The only incompatibility between the two stdlib lines is _≡?_ on ℤ → _≟_ (three sites in Prelude.agda). StepUp.agda needs nothing. Every other imported module and name exists in 2.1.
• PROOF-STATUS.md claimed the proofs "do not compile against v2.4 or v2.1". That was false; the line is replaced with the measured port note.
• Local run after the rebase, interface files deleted first, with the wrong Agda (2.7.0.1) first on PATH to show lib.sh resolves /usr/bin/agda ahead of it:

  check: Agda version 2.6.4.3, standard-library-2.1
  axiom-audit: auditing 7 module(s) … 7 module(s) reachable from CompositionalDA.All … clean
  check: CompositionalDA/All.agda type-checks
  gate-selftest: 18/18 controls behaved correctly
  check: OK
  

  Wall-clock 14:58:02Z → 15:00:00Z.
• Pkg.test(): 43/43, including the mutants in test/mutants.jl.

Files

• proofs/lib.sh (new) — toolchain resolution; dies naming what it found.
• proofs/check.sh (new) — the gate in CI order; replaces proofs/bootstrap.sh, which is deleted along with the vendoring and .agda-libraries machinery.
• proofs/tests/gate-selftest.sh — main's 18 controls unchanged; the bootstrap-based resolver block is replaced by sourcing lib.sh, and the libraries file is written by write_libraries.
• .github/workflows/ci.yml — proofs job rewritten to the Debian container recipe.
• README.md, proofs/PROOF-STATUS.md (toolchain paragraphs and a fresh "Last verified" block), .gitignore, proofs/.gitignore.

Merge

No required contexts on main (rules/branches/main is empty), so automerge is deliberately not armed; held for a human squash merge once the checks are green.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AjVQUkziVYywrLNsbPordh

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 34 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: aa359906-9b17-4511-aeb0-b87639ea4c07

📥 Commits

Reviewing files that changed from the base of the PR and between 320513d and 4843449.

📒 Files selected for processing (11)

• .github/workflows/ci.yml
• .gitignore
• README.md
• proofs/.gitignore
• proofs/PROOF-STATUS.md
• proofs/agda/CompositionalDA/Prelude.agda
• proofs/agda/compositionalda.agda-lib
• proofs/bootstrap.sh
• proofs/check.sh
• proofs/lib.sh
• proofs/tests/gate-selftest.sh

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Autopilot is currently an internal CodeRabbit preview.

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[hyperpolymath]

Conflict with main (after #2 merged) resolved in 2a5c5e4: a merge commit from main, not a rebase, so no force-push was needed.

• proofs/tests/gate-selftest.sh is Prove BH step-up (P5); gate self-test covers every audit check #2's 18-control version, ported to proofs/lib.sh (resolve_agda, resolve_stdlib, write_libraries). No bootstrap or vendor paths remain.
• proofs/PROOF-STATUS.md keeps Prove BH step-up (P5); gate self-test covers every audit check #2's content. Its toolchain, gate, reproducing and last-verified sections now describe Debian agda 2.6.4.3 + stdlib 2.1 and proofs/check.sh.
• StepUp.agda needed no change. Running proofs/check.sh on the merged tree gives exit 0, 7 modules audited clean and gate-selftest 18/18. A planted type error in StepUp is refused with exit 42.

Note for the session working in worktrees/CompositionalDA.jl-debian-pin: it was mid-git rebase origin/main at 14:57Z. This remote branch now has the merge on top, so git fetch before pushing. If you prefer your own resolution, replacing 2a5c5e4 is fine.

🤖 Generated with Claude Code