From 2b0d689d03177950598f49d5123727b03b50ce2b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 1 Oct 2026 14:08:20 +0100 Subject: [PATCH 1/2] docs(foundation): keep the 2026-05-18 history entries append-only PR #334 moved ABSZ_REF to f486c299 and, in passing, rewrote two dated 2026-05-18 entries in docs/foundation.adoc to name the new pin. Those entries record what was pinned in May; restore `3ff5cee` there and add a dated 2026-10-01 entry for the move. The current claims table and "Pinned inputs" keep f486c299. Answers the CodeRabbit thread on #334. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57 --- docs/foundation.adoc | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/docs/foundation.adoc b/docs/foundation.adoc index 23e6531..9acce59 100644 --- a/docs/foundation.adoc +++ b/docs/foundation.adoc @@ -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 `f486c29…` + library at tag `v2.3`, and `absolute-zero` at commit `3ff5cee…` (previously nixpkgs-bundled stdlib + a local `absolute-zero` checkout — neither reproducible). A hermetic `checks.suite` (guardrail + four roots + N5 xfail) runs under that pinned @@ -174,10 +174,17 @@ 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 @f486c29 as flake inputs, with a hermetic + + absolute-zero @3ff5cee 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 locally claimed green; flagged as such, gate unchanged. P1 item status moved from "tracked follow-up" to "implemented, pending first-green CI verification". +* *2026-10-01 — `absolute-zero` pin moved to the first green `Proofs` revision.* + `ABSZ_REF` in `.github/workflows/agda.yml` moved from `3ff5cee7` (2026-05-18) + to `f486c29903434589117fa0662c6f29b0f17d1d5f` (PR #334), the `absolute-zero` + revision whose own `Proofs` workflow is green on Coq, Lean, Agda and Z3 + (run 36864369380). The claims table and "Pinned inputs" above now read + `f486c299`; the two 2026-05-18 entries keep `3ff5cee` because they record + what was pinned then. Verified by `check` + `cold-check` green on #334. From 990b4058ca2b67dfac461f1d59a62e2e9a5af54d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 1 Oct 2026 14:08:57 +0100 Subject: [PATCH 2/2] docs(foundation): fix double-encoded em dash in the 2026-10-01 entry Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57 --- docs/foundation.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/foundation.adoc b/docs/foundation.adoc index 9acce59..6fa4b51 100644 --- a/docs/foundation.adoc +++ b/docs/foundation.adoc @@ -181,7 +181,7 @@ Pinned inputs: `standard-library` `v2.3`; `absolute-zero` locally claimed green; flagged as such, gate unchanged. P1 item status moved from "tracked follow-up" to "implemented, pending first-green CI verification". -* *2026-10-01 — `absolute-zero` pin moved to the first green `Proofs` revision.* +* *2026-10-01 — `absolute-zero` pin moved to the first green `Proofs` revision.* `ABSZ_REF` in `.github/workflows/agda.yml` moved from `3ff5cee7` (2026-05-18) to `f486c29903434589117fa0662c6f29b0f17d1d5f` (PR #334), the `absolute-zero` revision whose own `Proofs` workflow is green on Coq, Lean, Agda and Z3