Skip to content

Commit e63968c

Browse files
hyperpolymathclaude
andcommitted
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>
1 parent 137aaf9 commit e63968c

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)