ci: add reliable Agda job (version-matched agda-stdlib via git) (#106)

Gets Agda into CI **for real**, validated locally before pushing.

Root cause of the four earlier failures: Ubuntu's `agda-stdlib` apt
package ships sources with no usable library manifest. Fix: install just
the Agda binary via apt, then `git clone` **agda-stdlib v1.7.3**
(matches Agda 2.6.3) at a pinned tag, align its manifest `name:` to
`standard-library` (what the repo's `absolute-zero.agda-lib` depends
on), register, and type-check.

Locally confirmed: `CNO.agda` and `OND.agda` both type-check (exit 0)
with this exact toolchain. Coq + Z3 unchanged (already green).
`timeout-minutes: 25` guards the first-run stdlib compile.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.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