From e63968caff3f47ab7d1e7ffafb87383599695537 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 7 Jul 2026 06:40:33 +0100
Subject: [PATCH] fix(ci): point Agda at agda-stdlib sources via -i (no
 .agda-lib on Ubuntu)

Ubuntu's agda-stdlib package installs the library SOURCES to
/usr/share/agda-stdlib/ but ships no .agda-lib manifest, so library registration
cannot work. Instead add the stdlib root (parent of Data/Nat.agda) to Agda's
include path with -i. Coq + Z3 jobs already pass on the runner.

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

diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index 05ac750..daf2695 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -55,25 +55,19 @@ jobs:
       - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
       - name: Install Agda + stdlib
         run: sudo apt-get update && sudo apt-get install -y agda agda-stdlib
-      - name: Register the standard library
-        run: |
-          mkdir -p "$HOME/.agda"
-          # Grab whatever .agda-lib the package ships (name is version-dependent),
-          # with a filesystem fallback. Dump the file list on failure for triage.
-          LIB="$(dpkg -L agda-stdlib 2>/dev/null | grep -m1 '\.agda-lib$' || true)"
-          [ -z "$LIB" ] && LIB="$(find /usr -name '*.agda-lib' 2>/dev/null | grep -m1 -i 'standard' || true)"
-          if [ -z "$LIB" ]; then
-            echo "::error::no .agda-lib found for agda-stdlib"; dpkg -L agda-stdlib | tail -60; exit 1
-          fi
-          echo "$LIB" > "$HOME/.agda/libraries"
-          echo "standard-library" > "$HOME/.agda/defaults"
-          echo "registered: $LIB"
       - 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
+          # The Ubuntu agda-stdlib package installs the SOURCES (no .agda-lib
+          # manifest), so add its root directly to Agda's include path via -i.
+          # Locate the root as the parent of Data/Nat.agda (version-dir robust).
+          NAT="$(dpkg -L agda-stdlib | grep -m1 '/Data/Nat\.agda$')"
+          STDLIB="${NAT%/Data/Nat.agda}"
+          echo "stdlib include path: $STDLIB"
+          [ -d "$STDLIB" ] || { echo "::error::agda-stdlib source dir not found"; dpkg -L agda-stdlib | tail -60; exit 1; }
+          agda --safe --without-K -i "$STDLIB" CNO.agda
+          agda --safe --without-K -i "$STDLIB" OND.agda
           echo "✓ Agda: CNO + OND type-check"
 
   z3: