From 90dd1e2ad2c9569254e8abc37c0a1f6093044ba8 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 7 Jul 2026 11:19:05 +0100
Subject: [PATCH] =?UTF-8?q?ci:=20add=20reliable=20Agda=20job=20=E2=80=94?=
 =?UTF-8?q?=20git-cloned=20version-matched=20stdlib?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Validated locally: CNO.agda + OND.agda type-check (exit 0) with apt Agda 2.6.3
+ stock agda-stdlib v1.7.3 (name aligned to 'standard-library' to satisfy the
repo's absolute-zero.agda-lib depend). The four earlier failures were the wrong
stdlib source (Ubuntu's agda-stdlib ships no usable manifest); this fetches a
version-matched stdlib from git at a pinned tag. timeout-minutes guards the
first-run stdlib compile. Coq + Z3 unchanged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 .github/workflows/proofs.yml | 37 ++++++++++++++++++++++++++++--------
 1 file changed, 29 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index 2eee306..7ebe27d 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -48,14 +48,35 @@ jobs:
           make -f Makefile.all -j"$(nproc)"
           echo "✓ Coq: 14/14 theories compiled (CNO + OND)"
 
-  # NOTE: an Agda job was attempted but removed. Ubuntu's `agda-stdlib` package
-  # ships the sources without a usable library manifest, and the apt Agda/stdlib
-  # pairing on the runner would not resolve `standard-library` reliably across
-  # four different setups (register / -i include path / synthesized .agda-lib).
-  # Rather than ship a flaky red job, Agda is verified via the local/container
-  # gate `proofs/verify-all-provers.sh` (which type-checks CNO.agda + OND.agda).
-  # To re-add it, a pinned Agda toolchain (e.g. a Nix/setup-agda action with a
-  # matching agda-stdlib) is the reliable route — not apt.
+  agda:
+    name: Agda — CNO + OND
+    runs-on: ubuntu-24.04
+    timeout-minutes: 25
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
+      - name: Install Agda (binary only)
+        # Install just the `agda` binary (2.6.3 on 24.04). NOT `agda-stdlib` —
+        # the Ubuntu stdlib package ships no usable library manifest; we fetch a
+        # version-matched stdlib from git instead (validated locally).
+        run: sudo apt-get update && sudo apt-get install -y agda
+      - name: Fetch + register agda-stdlib v1.7.3 (matches Agda 2.6.3)
+        run: |
+          git clone -q --depth 1 --branch v1.7.3 \
+            https://github.com/agda/agda-stdlib.git "$HOME/agda-stdlib"
+          # The upstream manifest is named `standard-library-1.7.3`; the repo's
+          # absolute-zero.agda-lib depends on `standard-library`, so align it.
+          sed -i 's/^name: .*/name: standard-library/' \
+            "$HOME/agda-stdlib/standard-library.agda-lib"
+          mkdir -p "$HOME/.agda"
+          echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries"
+          echo "standard-library" > "$HOME/.agda/defaults"
+      - name: Type-check CNO + OND (--safe --without-K)
+        working-directory: proofs/agda
+        run: |
+          agda --version
+          agda --safe --without-K CNO.agda
+          agda --safe --without-K OND.agda
+          echo "✓ Agda: CNO + OND type-check"
 
   z3:
     name: Z3 — CNO + OND bounded checks