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 1/2] 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}" { From 92b662009bfcb93abf13f7a8993df82ca62e11e2 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 10:52:05 +0100 Subject: [PATCH 2/2] fix(ci): install the Idris2 support tree with the tree's own make target Second layer of the same omission, measured on #817's own run. The first fix copied `support/` as data, which cured the COMPILE-time error and exposed the RUN-time one: INTERNAL ERROR: Can't find data file chez/support.ss (compile) (while loading libidris2_support.so) cannot open shared object file: No such file or directory (run) `libidris2_support.so` is a BUILT C library, not a data file. The Chez backend copies it out of `/lib/` into the executable's `_app` directory at link time, so a build missing it still exits 0 and the failure only appears when the binary is first run -- one step later, inside the comparison, where it reads as a drift failure. Repairing this file by file is what produced the second failure. This commit stops doing that and uses the Idris2 tree's own targets instead: make -C support # builds the C library make -C install-support PREFIX=

# installs lib/ AND support/ which is complete by construction. `support/c/Makefile`'s own install target writes both `${PREFIX}/idris2-${VERSION}/lib` and `.../support/c`, so nothing is left to enumerate by hand. It costs seconds: it builds `support/` only, never the compiler. Measured on the CI runner, not assumed: prefix is `/home/runner/.idris2` and is writable, so no sudo is involved; the cache hit was on the shared key `idris2-v0.7.0-Linux-2`, confirming the omission comes from the sharing and not from a cold cache. The assertion now covers BOTH artefacts. The previous one checked only the compile-time file, which is precisely why the run-time one got through. Also asserts on the CONSUMER's artefact: after the build, that `build/abi-gen/exec/hypatia-abi-gen_app/libidris2_support.so` exists. A check on the producer proves nothing about the consumer -- the recurring guard/consumer trap -- and here the producer check genuinely passed while the consumer was broken. `Gen.idr` gains `--help` / `-h` exiting 0, so the build step can smoke- test that the binary actually RUNS. Missing arguments still print usage and exit 1: an explicit request for help succeeding and a usage error failing are different outcomes, and conflating them would have forced the workflow into an `|| true`, which is indistinguishable from a masked failure. Generated output is unaffected -- the provenance stamp hashes `Types.idr`, not `Gen.idr` -- and regeneration was verified byte- identical against all three tracked targets. Verified locally before pushing: --help / -h rc=0 no args / one arg rc=1 regenerate + diff connectors emitted: 16, 3 of 3, 0 drifted mutant: hand-edit generated Zig 1 drifted -> RED mutant: swap wire ids 3<->4 in the live Types.idr, no regen 3 drifted -> RED mutant: empty output dir compared 0 of 3 -> RED on the denominator positive control (clean tree) 3 of 3, 0 drifted -> GREEN The swap-ids mutant is the one that matters: it proves the gate reads the normative source, not merely that the generated copies agree with each other. Refs #120 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV --- .github/workflows/abi-codegen-drift.yml | 98 +++++++++++++++++++------ src/Hypatia/ABI/Gen.idr | 33 ++++++--- 2 files changed, 99 insertions(+), 32 deletions(-) diff --git a/.github/workflows/abi-codegen-drift.yml b/.github/workflows/abi-codegen-drift.yml index 0fdcd6f4..b4338b2d 100644 --- a/.github/workflows/abi-codegen-drift.yml +++ b/.github/workflows/abi-codegen-drift.yml @@ -76,41 +76,71 @@ 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. + # Building and RUNNING an Idris2 executable needs the Idris2 support + # installation: the Chez data tree at `/support/chez/support.ss` + # at compile time, and the compiled C library `/lib/ + # libidris2_support.so` -- which the Chez backend copies into the + # executable's `_app` directory -- at run time. Type-checking and + # building a LIBRARY needs neither. # - # `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 + # `verify-proofs.yml` only ever does the latter: `idris2 --check` over + # the proof files and `idris2 --build` on two library packages. It never + # links a binary. So the cache this job deliberately shares with it + # (same key, so the ~20-minute bootstrap is not repeated) was populated + # with NEITHER. Measured, not supposed -- twice, on PR #811 and #817: + # INTERNAL ERROR: Can't find data file chez/support.ss (compile) + # (while loading libidris2_support.so) cannot open shared object file + # (run) + # + # Sharing a warm cache imports its OMISSIONS as well as its contents. + # + # Hence the upstream install targets rather than copying files by hand: + # `make support` builds the C library, `make install-support` installs + # both it and the data tree to `/idris2-/{lib,support}`. + # Repairing this piece by piece is how the second failure happened; the + # tree's own target is complete by construction. It costs seconds -- it + # builds only `support/`, never the compiler. + - name: Ensure the Idris2 support installation is complete run: | set -euo pipefail + prefix="$(idris2 --prefix)" libdir="$(idris2 --libdir)" support="${libdir}/support" - if [ -f "${support}/chez/support.ss" ]; then - echo "chez support present: ${support}/chez/support.ss" + csolib="${libdir}/lib/libidris2_support.so" + + if [ -f "${support}/chez/support.ss" ] && [ -f "${csolib}" ]; then + echo "support installation already complete under ${libdir}" else - echo "chez support absent under ${support} -- installing from the Idris2 source tree" - rm -rf "${RUNNER_TEMP}/idris2-support-src" + echo "incomplete support installation under ${libdir}:" + echo " chez/support.ss: $([ -f "${support}/chez/support.ss" ] && echo present || echo ABSENT)" + echo " libidris2_support.so: $([ -f "${csolib}" ] && echo present || echo ABSENT)" + src="${RUNNER_TEMP}/idris2-support-src" + rm -rf "${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}/" + https://github.com/idris-lang/Idris2 "${src}" + make -C "${src}" support + make -C "${src}" install-support PREFIX="${prefix}" 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}" + + # Assert, do not assume, and assert BOTH -- the first fix asserted + # only the compile-time file and the job then died at run time on the + # other one. A missing support tree surfaces three steps later as an + # opaque INTERNAL ERROR, where it reads like a generator bug. + missing=0 + for f in "${support}/chez/support.ss" "${csolib}"; do + if [ ! -f "${f}" ]; then + echo "::error::missing after install-support: ${f}" + missing=$((missing + 1)) + fi + done + if [ "${missing}" -ne 0 ]; then if [ -d "${libdir}" ]; then - find "${libdir}" -maxdepth 3 -name 'support*' -print + find "${libdir}" -maxdepth 3 \( -name 'support*' -o -name 'libidris2_support*' \) -print fi exit 1 fi - echo "support tree: ${support}" + echo "support tree: ${support}" + echo "support lib: ${csolib}" - name: Build the generator run: | @@ -118,6 +148,28 @@ jobs: cd src/abi idris2 --build hypatia-abi-gen.ipkg + # Assert on the CONSUMER's artefact, not the installer's. The step + # above already checked that `/lib/libidris2_support.so` + # exists; this checks the thing that actually has to load it. The + # Chez backend COPIES that library into the executable's `_app` + # directory at link time, and a build missing it still exits 0 -- + # the failure only appears when the binary is first run, one step + # later, inside the comparison, where it reads as a drift failure. + # + # This is the guard/consumer trap: a check on the producer proves + # nothing about the consumer. Assert what the consumer needs. + app="../../build/abi-gen/exec/hypatia-abi-gen_app" + if [ ! -f "${app}/libidris2_support.so" ]; then + echo "::error::built executable is missing its runtime support library: ${app}/libidris2_support.so" + ls -la "${app}" || true + exit 1 + fi + + # Cheapest possible proof that the binary RUNS. `--help` exercises + # load + argument parsing and writes nothing, so it cannot mask a + # drift failure below by leaving output behind. + ../../build/abi-gen/exec/hypatia-abi-gen --help + - name: Regenerate into a temp dir and compare run: | set -euo pipefail diff --git a/src/Hypatia/ABI/Gen.idr b/src/Hypatia/ABI/Gen.idr index df8e299d..fa9659df 100644 --- a/src/Hypatia/ABI/Gen.idr +++ b/src/Hypatia/ABI/Gen.idr @@ -269,9 +269,12 @@ record Opts where constructor MkOpts outDir : Maybe String abiHash : Maybe String + help : Bool parseArgs : List String -> Opts -> Opts parseArgs [] acc = acc +parseArgs ("--help" :: rest) acc = parseArgs rest ({ help := True } acc) +parseArgs ("-h" :: rest) acc = parseArgs rest ({ help := True } acc) parseArgs ("--out-dir" :: v :: rest) acc = parseArgs rest ({ outDir := Just v } acc) parseArgs ("--abi-hash" :: v :: rest) acc = parseArgs rest ({ abiHash := Just v } acc) parseArgs (_ :: rest) acc = parseArgs rest acc @@ -297,15 +300,27 @@ emitAll outDir abiHash = do then pure () else exitFailure +usage : IO () +usage = do + putStrLn "usage: hypatia-abi-gen --out-dir

--abi-hash " + putStrLn "" + putStrLn " --out-dir directory to write the three generated files into" + putStrLn " --abi-hash `git hash-object src/Hypatia/ABI/Types.idr`" + putStrLn " --help, -h print this message and exit 0" + main : IO () main = do args <- getArgs - let opts = parseArgs (drop 1 args) (MkOpts Nothing Nothing) - case (opts.outDir, opts.abiHash) of - (Just o, Just h) => emitAll o h - _ => do - putStrLn "usage: hypatia-abi-gen --out-dir --abi-hash " - putStrLn "" - putStrLn " --out-dir directory to write the three generated files into" - putStrLn " --abi-hash `git hash-object src/Hypatia/ABI/Types.idr`" - exitFailure + let opts = parseArgs (drop 1 args) (MkOpts Nothing Nothing False) + -- An explicit `--help` is a successful request for help and exits 0; + -- MISSING arguments are a usage error and exit 1. Conflating the two makes + -- `--help` unusable as a smoke test, which is exactly what it is used for + -- in .github/workflows/abi-codegen-drift.yml -- and forces the caller into + -- an `|| true`, which is indistinguishable from a masked failure. + if opts.help + then usage + else case (opts.outDir, opts.abiHash) of + (Just o, Just h) => emitAll o h + _ => do + usage + exitFailure