Skip to content

Commit e9cc72e

Browse files
hyperpolymathclaude
andcommitted
fix(ci): synthesize agda-stdlib manifest (definitive Agda-job fix)
Root cause fully diagnosed: Ubuntu's agda-stdlib installs sources to /usr/share/agda-stdlib with NO .agda-lib manifest, so Agda fails with 'Library standard-library not found'. Create the manifest in the stdlib root (include: .) and register it in ~/.agda/libraries. Coq + Z3 already pass. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 720e410 commit e9cc72e

1 file changed

Lines changed: 17 additions & 9 deletions

File tree

.github/workflows/proofs.yml

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -55,19 +55,27 @@ 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: Synthesize + register the stdlib manifest
59+
run: |
60+
# Ubuntu's agda-stdlib installs the SOURCES to /usr/share/agda-stdlib
61+
# but ships NO .agda-lib manifest, so Agda can't resolve the
62+
# `standard-library` it expects. Create the manifest inside the stdlib
63+
# root (include: . = that dir) and register it in ~/.agda/libraries.
64+
NAT="$(dpkg -L agda-stdlib | grep -m1 '/Data/Nat\.agda$')"
65+
STDLIB="${NAT%/Data/Nat.agda}"
66+
echo "stdlib root: $STDLIB"
67+
[ -d "$STDLIB" ] || { echo "::error::agda-stdlib sources not found"; dpkg -L agda-stdlib | tail -60; exit 1; }
68+
printf 'name: standard-library\ninclude: .\n' | sudo tee "$STDLIB/standard-library.agda-lib" >/dev/null
69+
mkdir -p "$HOME/.agda"
70+
echo "$STDLIB/standard-library.agda-lib" > "$HOME/.agda/libraries"
71+
echo "standard-library" > "$HOME/.agda/defaults"
72+
echo "registered standard-library -> $STDLIB"
5873
- name: Type-check CNO + OND (--safe --without-K)
5974
working-directory: proofs/agda
6075
run: |
6176
agda --version
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
77+
agda --safe --without-K CNO.agda
78+
agda --safe --without-K OND.agda
7179
echo "✓ Agda: CNO + OND type-check"
7280
7381
z3:

0 commit comments

Comments
 (0)