Measured (2026-09-22, main = 9c4b72b)
.github/workflows/agda.yml:51 and :176 sudo apt-get install -y agda git (no version) on ubuntu-latest, with the stdlib cloned at v2.3.
- Positive control: epistemic-types'
Proof Safety runs in a digest-pinned debian:13-slim container with agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4, asserts agda --version, and passes --double-check; residual-evidence-types adopted the same recipe on 2026-09-22 (run 35773288367 green) with zero third-party actions.
- Three stdlib versions are in play across the family (2.1 in residual, 2.3 here, 2.1-4 distro in epistemic-types).
Why it matters
An image bump changes the prover under the proofs without a commit: the next ubuntu-latest rollover changes the apt agda version and no receipt records which one checked the suite.
Acceptance criteria
- Both steps install an explicit version (
agda-bin=<ver> in a digest-pinned container, or an apt pin with a checksum), and agda --version is asserted equal to the pinned string before any module is checked.
- Watched-failing → green:
grep -c 'apt-get install -y agda git' .github/workflows/agda.yml is 2 today, 0 after.
- The chosen stdlib version is recorded in PROOF-STATUS with the measured warning count under it (measure the
UnsupportedIndexedMatch warning count under each candidate stdlib before choosing; do not assume).
- Mutant: change the pinned version string to one that does not exist; the job fails at install, not silently later.
🤖 Generated with Claude Code
Measured (2026-09-22, main = 9c4b72b)
.github/workflows/agda.yml:51and:176sudo apt-get install -y agda git(no version) onubuntu-latest, with the stdlib cloned at v2.3.Proof Safetyruns in a digest-pinneddebian:13-slimcontainer withagda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4, assertsagda --version, and passes--double-check; residual-evidence-types adopted the same recipe on 2026-09-22 (run 35773288367 green) with zero third-party actions.Why it matters
An image bump changes the prover under the proofs without a commit: the next
ubuntu-latestrollover changes the aptagdaversion and no receipt records which one checked the suite.Acceptance criteria
agda-bin=<ver>in a digest-pinned container, or an apt pin with a checksum), andagda --versionis asserted equal to the pinned string before any module is checked.grep -c 'apt-get install -y agda git' .github/workflows/agda.ymlis 2 today, 0 after.UnsupportedIndexedMatchwarning count under each candidate stdlib before choosing; do not assume).🤖 Generated with Claude Code