Skip to content

Commit cdf87b3

Browse files
committed
ci(agda): install absolute-zero library so the suite typechecks
The echo-types.agda-lib declares `depend: standard-library absolute-zero`, but the workflow only registered standard-library. This has been red on main since 3f654ef (2026-04-30, EchoCNOBridge content-bridge promotion) added the dependency without updating CI. Adds a fetch step that shallow-clones hyperpolymath/absolute-zero, then registers it alongside standard-library in ~/.agda/libraries.
1 parent c72f45a commit cdf87b3

1 file changed

Lines changed: 15 additions & 2 deletions

File tree

.github/workflows/agda.yml

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,14 @@ jobs:
3030
git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
3131
echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"
3232
33-
- name: Register standard library for Agda
33+
- name: Fetch absolute-zero library
34+
id: absz
35+
run: |
36+
ABSZ_DIR="$RUNNER_TEMP/absolute-zero"
37+
git clone --depth 1 https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR"
38+
echo "absz_dir=$ABSZ_DIR" >> "$GITHUB_OUTPUT"
39+
40+
- name: Register libraries for Agda
3441
run: |
3542
mkdir -p "$HOME/.agda"
3643
@@ -40,7 +47,13 @@ jobs:
4047
include: ${{ steps.stdlib.outputs.stdlib_dir }}/src
4148
EOF
4249
43-
printf '%s\n' "$STDLIB_LIB" > "$HOME/.agda/libraries"
50+
ABSZ_LIB="$RUNNER_TEMP/absolute-zero.agda-lib"
51+
cat > "$ABSZ_LIB" <<EOF
52+
name: absolute-zero
53+
include: ${{ steps.absz.outputs.absz_dir }}/proofs/agda
54+
EOF
55+
56+
printf '%s\n%s\n' "$STDLIB_LIB" "$ABSZ_LIB" > "$HOME/.agda/libraries"
4457
printf '%s\n' "standard-library" > "$HOME/.agda/defaults"
4558
4659
- name: Typecheck full suite

0 commit comments

Comments
 (0)