From c82e9aaf0ab26d6f9cd27d6ee6665d78b1acd6ee Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 10:45:25 +0100 Subject: [PATCH] fix(ci): install the Chez support tree so the ABI drift gate can pass The gate added in #811 failed on its own pull request and is now red on main. The failure is real and the cause is measured, not supposed: INTERNAL ERROR: Can't find data file chez/support.ss in any of ["/home/runner/.idris2/idris2-0.7.0/support/chez/support.ss", ...] Compiling an Idris2 EXECUTABLE needs the Chez support tree at `$(idris2 --libdir)/support/chez/support.ss`; type-checking and building a LIBRARY does not. `verify-proofs.yml` only ever does the latter -- it runs `idris2 --check` and `idris2 --build` on library packages and never links a binary -- so the cache this job deliberately shares with it (same key `idris2-${IDRIS2_VERSION}-${runner.os}-2`) was populated without that tree. Sharing a warm cache imports its omissions as well as its contents. `support/` is plain data (Scheme and C sources shipped in the Idris2 repo). It needs no build, so a shallow clone at the pinned tag repairs it in seconds rather than repeating the ~20-minute bootstrap. The new step then asserts the file is present BY NAME. Previously a missing support tree surfaced as an opaque INTERNAL ERROR three steps later, inside the generator build, where it read like a generator bug. Also in this commit: `zig.yml` extracted the test count with `grep ... || true`, which the Hypatia workflow scanner flagged at zig.yml:99 as swallowing a non-zero exit. `set -o pipefail` already made a genuine `zig test` failure fatal, so nothing was actually masked -- but a suppressed exit code is indistinguishable from a masked failure to a reader or a scanner, so the extraction is rewritten in awk, which exits 0 whether or not it matched and therefore needs no suppression at all. The count check below it is now the only thing that can fail the step. Measured against the real `zig test` output (4) and against three mutant logs (all 0, all red). The last `|| true` in abi-codegen-drift.yml -- a diagnostic `find` inside an already-failing branch -- is replaced by a `[ -d ]` guard for the same reason. Not addressed here, and not caused by this change: `governance / Actions lockfile verify` is red because #810 bumped 7 actions without refreshing `.github/workflows/actions.lock`. Filed separately. Refs #120 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV --- .github/workflows/abi-codegen-drift.yml | 36 +++++++++++++++++++++++++ .github/workflows/zig.yml | 26 +++++++++++++----- 2 files changed, 56 insertions(+), 6 deletions(-) diff --git a/.github/workflows/abi-codegen-drift.yml b/.github/workflows/abi-codegen-drift.yml index 505928b3..0fdcd6f4 100644 --- a/.github/workflows/abi-codegen-drift.yml +++ b/.github/workflows/abi-codegen-drift.yml @@ -76,6 +76,42 @@ jobs: - name: Verify Idris is on PATH run: idris2 --version + # Compiling an EXECUTABLE needs the Chez support tree + # (`/support/chez/support.ss`); type-checking and building a + # LIBRARY does not. `verify-proofs.yml` only ever does the latter, so the + # cache this job deliberately shares with it was populated without that + # tree and this job died at + # INTERNAL ERROR: Can't find data file chez/support.ss + # on its very first run. Measured, not supposed: PR #811's gate run. + # + # `support/` is plain data (Scheme and C sources shipped in the Idris2 + # repo); it needs no build, so a shallow clone is enough to repair it. + - name: Ensure the Chez support tree is installed + run: | + set -euo pipefail + libdir="$(idris2 --libdir)" + support="${libdir}/support" + if [ -f "${support}/chez/support.ss" ]; then + echo "chez support present: ${support}/chez/support.ss" + else + echo "chez support absent under ${support} -- installing from the Idris2 source tree" + rm -rf "${RUNNER_TEMP}/idris2-support-src" + git clone --depth 1 --branch "${IDRIS2_VERSION}" \ + https://github.com/idris-lang/Idris2 "${RUNNER_TEMP}/idris2-support-src" + mkdir -p "${support}" + cp -R "${RUNNER_TEMP}/idris2-support-src/support/." "${support}/" + fi + # Assert, do not assume. A missing support tree previously surfaced as + # an opaque INTERNAL ERROR three steps later; fail here, by name. + if [ ! -f "${support}/chez/support.ss" ]; then + echo "::error::chez/support.ss still missing under ${support}" + if [ -d "${libdir}" ]; then + find "${libdir}" -maxdepth 3 -name 'support*' -print + fi + exit 1 + fi + echo "support tree: ${support}" + - name: Build the generator run: | set -euo pipefail diff --git a/.github/workflows/zig.yml b/.github/workflows/zig.yml index 458dd8f4..a7d88b19 100644 --- a/.github/workflows/zig.yml +++ b/.github/workflows/zig.yml @@ -103,12 +103,26 @@ jobs: zig test ffi/zig/src/unified-api-adapter.zig 2>&1 | tee "${RUNNER_TEMP}/zig-test.log" # The denominator. `zig test` on a file containing no `test` blocks - # exits 0 -- a green tick that proves nothing. Insist that it says - # how many it ran, and that the number is not zero. - summary=$(grep -Eo '[0-9]+ of [0-9]+ test[s]? passed|All [0-9]+ tests passed' \ - "${RUNNER_TEMP}/zig-test.log" | tail -1 || true) - count=$(printf '%s' "${summary}" | grep -Eo '[0-9]+' | tail -1 || true) - count=${count:-0} + # exits 0 and prints "All 0 tests passed." -- a green tick that proves + # nothing. Insist that it says how many it ran, and that it is not 0. + # + # awk, not `grep ... || true`: grep exits 1 when it matches nothing, + # which under `set -e` needs suppressing, and a suppressed exit code + # is indistinguishable from a masked failure to a reader or a + # scanner. awk exits 0 whether or not it matched, so the no-match + # case needs no suppression and the check below stays the only thing + # that can fail this step. + count=$(awk ' + match($0, /All [0-9]+ tests passed/) || + match($0, /[0-9]+ of [0-9]+ tests? passed/) { last = $0 } + END { + n = 0 + while (match(last, /[0-9]+/)) { + n = substr(last, RSTART, RLENGTH) + last = substr(last, RSTART + RLENGTH) + } + print n + 0 + }' "${RUNNER_TEMP}/zig-test.log") echo "zig tests run: ${count}" {