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