From 183a43713b3d0ce94288cbf09b64d43a4969ee39 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:51:48 +0100 Subject: [PATCH] chore(agda): bump absolute-zero pin 3ff5cee7 -> f486c299 (Proofs green on main) absolute-zero main was red on Coq and Lean from #174 (2026-09-26) until #177 squashed as f486c299 on 2026-10-01; the Proofs run on that commit is green for Coq, Lean and Z3. Pin the first green revision, per the rule that a pin names a revision whose own gate passed. Both ABSZ_REF sites in agda.yml and the four references in docs/foundation.adoc move together; no Agda source changes. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57 --- .github/workflows/agda.yml | 6 +++--- docs/foundation.adoc | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) 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