From 5d91cdf2b4920c5853423fc97170f5096574f989 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 16:59:37 +0000 Subject: [PATCH 1/2] ci(agda): typecheck the experimental echo-additive tree standalone Adds a lane (warm and cold) that typechecks every module under proofs/agda/experimental/echo-additive/ on its own. Nothing is added to All.agda or Smoke.agda, so the shipped closure and its claims are unchanged (D-2026-06-14-R1 firewall; R-2026-05-18 stands). A consumer that vendors Grade.agda (choreographic-types) now learns here when an edit breaks it. Verified locally under Agda 2.6.3 / stdlib v2.3 / absolute-zero f486c29: all seven modules exit 0; check-guardrails.sh passes. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- .github/workflows/agda.yml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index b770357..ca93b16 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -157,6 +157,20 @@ jobs: - name: Typecheck cubical lane (epi/mono truncation discharge) run: agda -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda + # Experimental lane: the echo-additive grade tree. Each module is + # typechecked STANDALONE (--safe --without-K from its own pragma); + # nothing here is imported by All.agda or Smoke.agda, so it adds + # no claim to the shipped closure (D-2026-06-14-R1 firewall, and + # R-2026-05-18 stands). What it does buy: downstream consumers + # that vendor Grade.agda (choreographic-types) learn here, not + # in their own CI, when an edit breaks it. + - name: Typecheck experimental echo-additive lane (standalone, not in the closure) + run: | + for f in proofs/agda/experimental/echo-additive/*.agda; do + echo "== $f" + agda -i proofs/agda "$f" + done + cold-check: # Belt-and-braces: NO interface cache, --ignore-interfaces cold # build. A green here cannot be a stale-.agdai artefact (matters @@ -201,3 +215,7 @@ jobs: agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda agda --ignore-interfaces -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda + for f in proofs/agda/experimental/echo-additive/*.agda; do + echo "== $f" + agda --ignore-interfaces -i proofs/agda "$f" + done From 52c1ef5422c2e140bb4236f29a1a7b5fb8266c35 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 17:13:43 +0000 Subject: [PATCH 2/2] ci(agda): check the echo-additive tree through one aggregate root Codex review on #343: the cold lane started a fresh Agda process per module with --ignore-interfaces, rebuilding the standard library seven times inside the job's 30-minute cap. proofs/agda/experimental/echo-additive/All.agda imports the seven modules; both the warm and cold steps now check that one root. Cold, locally: exit 0 in 95 s. Not imported by the shipped All.agda or Smoke.agda. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- .github/workflows/agda.yml | 15 ++++-------- .../agda/experimental/echo-additive/All.agda | 24 +++++++++++++++++++ 2 files changed, 28 insertions(+), 11 deletions(-) create mode 100644 proofs/agda/experimental/echo-additive/All.agda diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index ca93b16..5637283 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -157,19 +157,15 @@ jobs: - name: Typecheck cubical lane (epi/mono truncation discharge) run: agda -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda - # Experimental lane: the echo-additive grade tree. Each module is - # typechecked STANDALONE (--safe --without-K from its own pragma); + # Experimental lane: the echo-additive grade tree, typechecked through + # its own aggregate root (--safe --without-K from the pragmas); # nothing here is imported by All.agda or Smoke.agda, so it adds # no claim to the shipped closure (D-2026-06-14-R1 firewall, and # R-2026-05-18 stands). What it does buy: downstream consumers # that vendor Grade.agda (choreographic-types) learn here, not # in their own CI, when an edit breaks it. - name: Typecheck experimental echo-additive lane (standalone, not in the closure) - run: | - for f in proofs/agda/experimental/echo-additive/*.agda; do - echo "== $f" - agda -i proofs/agda "$f" - done + run: agda -i proofs/agda proofs/agda/experimental/echo-additive/All.agda cold-check: # Belt-and-braces: NO interface cache, --ignore-interfaces cold @@ -215,7 +211,4 @@ jobs: agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda agda --ignore-interfaces -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda - for f in proofs/agda/experimental/echo-additive/*.agda; do - echo "== $f" - agda --ignore-interfaces -i proofs/agda "$f" - done + agda --ignore-interfaces -i proofs/agda proofs/agda/experimental/echo-additive/All.agda diff --git a/proofs/agda/experimental/echo-additive/All.agda b/proofs/agda/experimental/echo-additive/All.agda new file mode 100644 index 0000000..c71a56a --- /dev/null +++ b/proofs/agda/experimental/echo-additive/All.agda @@ -0,0 +1,24 @@ +{-# OPTIONS --safe --without-K #-} + +-- EXPERIMENTAL aggregate root for CI only. +-- +-- Typechecking this one file typechecks the whole echo-additive tree in a +-- single pass, so a cold (--ignore-interfaces) run builds the shared standard +-- library once instead of once per module. +-- +-- NOT imported by proofs/agda/All.agda or Smoke.agda, and nothing in shipped +-- code imports from experimental/ (D-2026-06-14-R1 firewall; R-2026-05-18 +-- stands). It adds no claim to the shipped closure. +-- +-- Add any new module under experimental/echo-additive/ here, or CI will not +-- check it. + +module experimental.echo-additive.All where + +open import experimental.echo-additive.Grade +open import experimental.echo-additive.VarianceGate +open import experimental.echo-additive.GradedCarrier +open import experimental.echo-additive.GradedCarrierFaithful +open import experimental.echo-additive.GradedMonad +open import experimental.echo-additive.GradedComonad +open import experimental.echo-additive.GradedAdjunction