Skip to content

fix(ci): complete the Idris2 support install so abi-codegen-drift can pass #819

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Sep 22, 2026
Merged

fix(ci): complete the Idris2 support install so abi-codegen-drift can pass #819

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
114 changes: 91 additions & 23 deletions .github/workflows/abi-codegen-drift.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,48 +76,116 @@ jobs:
- name: Verify Idris is on PATH
run: idris2 --version

# Compiling an EXECUTABLE needs the Chez support tree
# (`<libdir>/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 `<libdir>/support/chez/support.ss`
# at compile time, and the compiled C library `<libdir>/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 `<prefix>/idris2-<version>/{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: |
set -euo pipefail
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 `<libdir>/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
Expand Down
33 changes: 24 additions & 9 deletions src/Hypatia/ABI/Gen.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -297,15 +300,27 @@ emitAll outDir abiHash = do
then pure ()
else exitFailure

usage : IO ()
usage = do
putStrLn "usage: hypatia-abi-gen --out-dir <dir> --abi-hash <hex>"
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 <dir> --abi-hash <hex>"
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
Loading