From 7b5b5ab0139b83f3d9fe55a34aa79aef92f35e1d 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] fix(ci): install the Idris2 support tree with the tree's own make target PR #817 squash-merged at head c82e9aa, which carried only the first half of this fix. `abi-codegen-drift` on main (5060161) is still red. This carries the remainder. The gate needs two support artefacts that were absent under `$(idris2 --libdir)` on the runner: INTERNAL ERROR: Can't find data file chez/support.ss (compile time) (while loading libidris2_support.so) cannot open shared object file (run time) #817 cured the first by copying `support/` in as data. That is not sufficient: `libidris2_support.so` is a BUILT C library, not data, and the Chez backend copies it into the executable's `_app` directory at link time. Repairing an incomplete installation file by file reveals one layer per CI round trip, so this uses the tree's own targets instead, which are complete by construction: make -C support make -C install-support PREFIX="$(idris2 --prefix)" It builds `support/` only, never the compiler, and costs seconds. Corrects the cause recorded in #817. It is NOT that library builds do not need the support tree. Idris2's Makefile has install: install-idris2 install-support install-libs so verify-proofs.yml's `sudo make install PREFIX=/usr/local` does install it -- under /usr/local/idris2-0.7.0. The binary resolves `--libdir` to /home/runner/.idris2/idris2-0.7.0. It is a PREFIX MISMATCH, and that job's cache `path:` list names both prefixes. Library work never needs the difference, which is why only a job linking an executable noticed. Also: * Assert on the CONSUMER's artefact. #817 asserted the installer's output and the job still died at run time. This checks `build/abi-gen/exec/hypatia-abi-gen_app/libidris2_support.so` -- the thing that actually has to load it -- and smoke-tests the binary with `--help`. * `Gen.idr`: `--help` now exits 0. It exited 1, so under `set -e` the smoke test would have forced an `|| true`, which is indistinguishable from a masked failure. Missing arguments remain a usage error and still exit 1. Verified locally before pushing: `--help`/`-h` rc=0, no-args and one-arg rc=1, regeneration prints `connectors emitted: 16` / `files written: 3 of 3` with zero diff against all three tracked targets, and all four mutants behave -- clean tree green; hand-edited generated Zig 1 drifted; wire ids 3<->4 swapped in the live Types.idr without regenerating 3 drifted (the one proving the gate reads the normative source, not merely that the copies agree); empty output dir fails on the denominator at `compared 0 of 3`. Refs #120, #811, #817 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV --- .github/workflows/abi-codegen-drift.yml | 114 +++++++++++++++++++----- src/Hypatia/ABI/Gen.idr | 33 +++++-- 2 files changed, 115 insertions(+), 32 deletions(-) diff --git a/.github/workflows/abi-codegen-drift.yml b/.github/workflows/abi-codegen-drift.yml index 0fdcd6f4..83c24f83 100644 --- a/.github/workflows/abi-codegen-drift.yml +++ b/.github/workflows/abi-codegen-drift.yml @@ -76,41 +76,87 @@ 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. # - # `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 + # Neither was present under `$(idris2 --libdir)` on this runner. + # 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) + # + # Why they are missing is a PREFIX MISMATCH, not a missing install step. + # Idris2's top-level Makefile is + # install: install-idris2 install-support install-libs + # so `verify-proofs.yml`'s `sudo make install PREFIX=/usr/local` DOES + # install support -- under `/usr/local/idris2-0.7.0/`. But the binary + # resolves `idris2 --libdir` to `/home/runner/.idris2/idris2-0.7.0`, and + # that job's cache `path:` list names both prefixes. Library work + # (`idris2 --check`, `--build` on the two proof packages) never needs the + # difference, so it went unnoticed until a job here linked an executable. + # + # Two rules follow, and this step obeys both: + # * a warm cache shared with another workflow imports that workflow's + # OMISSIONS as well as its contents -- ask what the populating job + # never did, not merely whether the key hits; + # * anchor on `$(idris2 --libdir)` / `$(idris2 --prefix)`, never on the + # PREFIX someone passed to `make install`. They can differ silently. + # + # 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. + # + # Note the repair is deliberately NOT persisted: `Post Cache` is skipped + # on a cache hit, so this job never mutates the shared entry and redoes + # the clone+build each run. Do not "optimise" that away -- two workflows + # writing one cache key is how the poisoned cache of -1 happened. + - 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 +164,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