Skip to content

Commit 137aaf9

Browse files
fix(ci): robust agda-stdlib registration (green the proofs workflow) (#103)
The Agda job in `proofs.yml` failed on `main` (PR #102) with `agda-stdlib .agda-lib not found` — a too-narrow grep, not a proof regression. Coq and Z3 jobs pass on the runner. This matches any `*.agda-lib` the package ships, with a filesystem fallback and a diagnostic dump. Greens the workflow on main. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 42b2001 commit 137aaf9

1 file changed

Lines changed: 9 additions & 7 deletions

File tree

.github/workflows/proofs.yml

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -58,14 +58,16 @@ jobs:
5858
- name: Register the standard library
5959
run: |
6060
mkdir -p "$HOME/.agda"
61-
LIB="$(dpkg -L agda-stdlib | grep -m1 'standard-library.*\.agda-lib' || true)"
62-
if [ -n "$LIB" ]; then
63-
echo "$LIB" > "$HOME/.agda/libraries"
64-
echo "standard-library" > "$HOME/.agda/defaults"
65-
echo "registered: $LIB"
66-
else
67-
echo "agda-stdlib .agda-lib not found via dpkg -L" >&2; exit 1
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
6867
fi
68+
echo "$LIB" > "$HOME/.agda/libraries"
69+
echo "standard-library" > "$HOME/.agda/defaults"
70+
echo "registered: $LIB"
6971
- name: Type-check CNO + OND (--safe --without-K)
7072
working-directory: proofs/agda
7173
run: |

0 commit comments

Comments
 (0)