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

[hyperpolymath]

Why this exists

PR #817 was squash-merged at head c82e9aa, which carried only the first
half of the fix. The second commit landed on the branch after the merge and
is not in main. Measured, not assumed:

$ gh api repos/hyperpolymath/hypatia/commits/5060161.../check-runs
completed  failure  abi-codegen-drift

abi-codegen-drift — the gate #811 shipped — is still red on main. This
PR carries the remainder.

What was actually wrong

Running (not merely building) an Idris2 executable needs two support artefacts,
and neither was present under $(idris2 --libdir) on the runner:

artefact	when it is needed	symptom
<libdir>/support/chez/support.ss	compile	INTERNAL ERROR: Can't find data file chez/support.ss
<libdir>/lib/libidris2_support.so	run	(while loading libidris2_support.so) cannot open shared object file

#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. Fixing an
incomplete installation file-by-file reveals one layer per CI round trip, which
is exactly how the second failure happened. So this uses the tree's own
targets, which are complete by construction:

make -C "$src" support
make -C "$src" install-support PREFIX="$(idris2 --prefix)"

It builds support/ only, never the compiler — seconds, not a bootstrap.

⚠ It corrects the cause #817 recorded

#817 says library builds do not need the support tree, so the shared cache
never had it. That is false, and the evidence was already in the repo.
Idris2's top-level Makefile:

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/. The binary resolves
idris2 --libdir to /home/runner/.idris2/idris2-0.7.0, and that job's cache
path: list names both prefixes. It is a prefix mismatch. Library work
(--check, --build on the two proof packages) never needs the difference,
which is why only a job linking an executable ever noticed.

The fix is correct either way because it anchors on $(idris2 --libdir) /
$(idris2 --prefix) rather than on a hard-coded prefix — but the comment in
the workflow now says what was measured instead of the tidier story.

Two further changes

Assert on the consumer's artefact. #817 asserted the installer's output
and the job still died at run time. This asserts
build/abi-gen/exec/hypatia-abi-gen_app/libidris2_support.so — the thing that
actually has to load it — because a build missing that copy still exits 0, and
the failure then surfaces one step later inside the comparison, where it reads
as a drift failure rather than a toolchain fault. Plus a --help smoke test:
the cheapest proof the binary runs, and it writes nothing, so it cannot mask a
drift failure by leaving output behind.

Gen.idr: --help exits 0. It exited 1, so under set -e the smoke test
would have failed and tempted an || true — the exact pattern the Hypatia
scanner flags and which is indistinguishable from a masked failure. Missing
arguments are still a usage error and still exit 1.

Verification done 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.
• Mutants, against the gate's own comparison logic:

case	compared	drifted	verdict
positive control (clean tree)	3 of 3	0	green
hand-edit generated Zig (arrow_flight→arrowflight)	3 of 3	1	red
swap wire ids 3↔4 in the live Types.idr, no regen	3 of 3	3	red
empty output dir	0 of 3	3	red on the denominator

The third is the decisive one: it proves the gate reads the normative
source, not merely that the generated copies agree with each other.

Note on caching

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. That is the intended property and should not be "optimised" away;
two workflows writing one cache key is how the poisoned -1 cache happened.

Not blockers (pre-existing on main, per the standing ruling)

governance / Actions lockfile verify (#818, from #810) · Check / Test /
Clippy / Cargo check + clippy + fmt (#814) · governance / {Code quality + docs, Validate Hypatia Baseline, Workflow security linter} ·
CodeQL Security Analysis startup failure. None are touched by this diff.

Refs #120, #811, #817

🤖 Generated with Claude Code

https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: f4da26c5-32c4-4a7e-905b-2d620c42a6a5

📥 Commits

Reviewing files that changed from the base of the PR and between 5060161 and 7b5b5ab.

📒 Files selected for processing (2)

• .github/workflows/abi-codegen-drift.yml
• src/Hypatia/ABI/Gen.idr

 _______________________________________________________
< Perhaps loot boxes can help us cover the OpenAI bill. >
 -------------------------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}