Skip to content

Commit 720e410

Browse files
fix(ci): Agda job — use -i stdlib sources (Ubuntu ships no .agda-lib) (#104)
Second and final Agda-job fix. Root cause: Ubuntu's `agda-stdlib` installs sources under `/usr/share/agda-stdlib/` with **no `.agda-lib` manifest**, so registration was doomed. This adds the stdlib root to Agda's include path via `-i` (located as the parent of `Data/Nat.agda`). Coq + Z3 already pass. If this still fights the runner, next step is to drop Agda from CI (covered by `proofs/verify-all-provers.sh`). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 137aaf9 commit 720e410

1 file changed

Lines changed: 9 additions & 15 deletions

File tree

.github/workflows/proofs.yml

Lines changed: 9 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -55,25 +55,19 @@ jobs:
5555
- uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
5656
- name: Install Agda + stdlib
5757
run: sudo apt-get update && sudo apt-get install -y agda agda-stdlib
58-
- name: Register the standard library
59-
run: |
60-
mkdir -p "$HOME/.agda"
61-
# Grab whatever .agda-lib the package ships (name is version-dependent),
62-
# with a filesystem fallback. Dump the file list on failure for triage.
63-
LIB="$(dpkg -L agda-stdlib 2>/dev/null | grep -m1 '\.agda-lib$' || true)"
64-
[ -z "$LIB" ] && LIB="$(find /usr -name '*.agda-lib' 2>/dev/null | grep -m1 -i 'standard' || true)"
65-
if [ -z "$LIB" ]; then
66-
echo "::error::no .agda-lib found for agda-stdlib"; dpkg -L agda-stdlib | tail -60; exit 1
67-
fi
68-
echo "$LIB" > "$HOME/.agda/libraries"
69-
echo "standard-library" > "$HOME/.agda/defaults"
70-
echo "registered: $LIB"
7158
- name: Type-check CNO + OND (--safe --without-K)
7259
working-directory: proofs/agda
7360
run: |
7461
agda --version
75-
agda --safe --without-K CNO.agda
76-
agda --safe --without-K OND.agda
62+
# The Ubuntu agda-stdlib package installs the SOURCES (no .agda-lib
63+
# manifest), so add its root directly to Agda's include path via -i.
64+
# Locate the root as the parent of Data/Nat.agda (version-dir robust).
65+
NAT="$(dpkg -L agda-stdlib | grep -m1 '/Data/Nat\.agda$')"
66+
STDLIB="${NAT%/Data/Nat.agda}"
67+
echo "stdlib include path: $STDLIB"
68+
[ -d "$STDLIB" ] || { echo "::error::agda-stdlib source dir not found"; dpkg -L agda-stdlib | tail -60; exit 1; }
69+
agda --safe --without-K -i "$STDLIB" CNO.agda
70+
agda --safe --without-K -i "$STDLIB" OND.agda
7771
echo "✓ Agda: CNO + OND type-check"
7872
7973
z3:

0 commit comments

Comments
 (0)