diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index bbb86b9..b770357 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -78,11 +78,11 @@ jobs: - name: Fetch absolute-zero library (PINNED) id: absz env: - # Pinned 2026-05-18 to the known-good revision the suite is + # Pinned 2026-10-01 (was 3ff5cee7, 2026-05-18) to the known-good revision the suite is # green against (foundation provenance audit). Bump # deliberately, never float: an unpinned dependency is an # unpinned trust boundary. - ABSZ_REF: 3ff5cee7f3fd002378089cd02f0c90a3747b45f0 + ABSZ_REF: f486c29903434589117fa0662c6f29b0f17d1d5f run: | ABSZ_DIR="$HOME/absolute-zero" git clone https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR" @@ -181,7 +181,7 @@ jobs: - name: Fetch pinned libraries id: libs env: - ABSZ_REF: 3ff5cee7f3fd002378089cd02f0c90a3747b45f0 + ABSZ_REF: f486c29903434589117fa0662c6f29b0f17d1d5f run: | STDLIB_DIR="$HOME/agda-stdlib" git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR" diff --git a/docs/foundation.adoc b/docs/foundation.adoc index 97d10aa..23e6531 100644 --- a/docs/foundation.adoc +++ b/docs/foundation.adoc @@ -67,7 +67,7 @@ claimed. | Dependencies are pinned | `standard-library` pinned to branch `v2.3`; `absolute-zero` pinned - to commit `3ff5cee7…` (was floating `--depth 1`). Asserted in CI. + to commit `f486c299…` (was floating `--depth 1`). Asserted in CI. | Agda version itself — see *Known limitations* |=== @@ -94,7 +94,7 @@ hack: left explicit and failing, never forced green. . *CI Agda exact pin* — *reproducible pin IMPLEMENTED 2026-05-18; first-green verification delegated to CI.* `flake.guix` now pins, as flake inputs: Agda via `nixpkgs nixos-24.11` (2.7.0.1), standard - library at tag `v2.3`, and `absolute-zero` at commit `3ff5cee…` + library at tag `v2.3`, and `absolute-zero` at commit `f486c29…` (previously nixpkgs-bundled stdlib + a local `absolute-zero` checkout — neither reproducible). A hermetic `checks.suite` (guardrail + four roots + N5 xfail) runs under that pinned @@ -151,7 +151,7 @@ agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda ---- Pinned inputs: `standard-library` `v2.3`; `absolute-zero` -`3ff5cee7f3fd002378089cd02f0c90a3747b45f0`. Agda: see `flake.guix` +`f486c29903434589117fa0662c6f29b0f17d1d5f`. Agda: see `flake.guix` (reproducible) — CI parity is the P1 item above. == Revision history @@ -174,7 +174,7 @@ Pinned inputs: `standard-library` `v2.3`; `absolute-zero` a divergent entry on this `main`-based branch would fork it). * *2026-05-18 — CI-via-flake reproducible pin implemented.* `flake.guix` evolved to pin Agda (nixpkgs nixos-24.11) + stdlib v2.3 - + absolute-zero @3ff5cee as flake inputs, with a hermetic + + absolute-zero @f486c29 as flake inputs, with a hermetic `checks.suite`; additive `flake-check` CI job (`continue-on-error`) added as the verifier. Authored without local `guix` (none in dev env) — designed-correct, CI-verified, not