verify-proofs.yml installs Idris2 to PREFIX=/usr/local but the binary reads --libdir under ~/.idris2 #820

Summary

verify-proofs.yml bootstraps Idris2 with sudo make install PREFIX=/usr/local,
but the resulting binary resolves idris2 --libdir to ~/.idris2/idris2-0.7.0.
Two prefixes are in play in one job, and the cache path: list names both.
This cost two CI round trips on #817 and #819 and forces
abi-codegen-drift.yml to carry a repair step it should not need.

Evidence

Idris2's top-level Makefile:

install: install-idris2 install-support install-libs

So the support tree is installed by that command — under
/usr/local/idris2-0.7.0/{lib,support}. But the runner reports:

$ idris2 --libdir
/home/runner/.idris2/idris2-0.7.0

and neither <libdir>/support/chez/support.ss nor
<libdir>/lib/libidris2_support.so was present there, producing:

INTERNAL ERROR: Can't find data file chez/support.ss              (compile)
(while loading libidris2_support.so) cannot open shared object file    (run)

The cache step already hedges across both locations:

path: |
  /usr/local/bin/idris2
  /usr/local/bin/idris2_app
  /usr/local/lib/idris2
  ~/.idris2

verify-proofs.yml itself does not notice, because everything it does is
library work — idris2 --check over the proof files and idris2 --build on
src/abi/hypatia-abi.ipkg and verify/hypatia-verify.ipkg. Library
type-checking and building never need the two artefacts above. Only a job that
links and runs an executable does, which is why abi-codegen-drift was the
first to hit it.

Why it matters

.github/workflows/abi-codegen-drift.yml now carries an "Ensure the Idris2
support installation is complete" step (PR #819) that clones the Idris2 source
and runs make support + make install-support PREFIX="$(idris2 --prefix)" on
every run — because Post Cache is skipped on a cache hit, so the repair is
never persisted. It costs seconds, not a bootstrap, so this is not urgent. But
it is a workaround for a bootstrap that installs to a prefix the binary does
not read.

Acceptance criteria

1. Print, in a CI run of verify-proofs.yml, all four of:
   idris2 --prefix, idris2 --libdir,
   ls /usr/local/idris2-0.7.0/ and ls ~/.idris2/idris2-0.7.0/
   — establishing by measurement which prefix holds what. Do not infer.
2. Decide, on that evidence, one of:
   • set IDRIS2_PREFIX=/usr/local (or equivalent) so --libdir resolves to
     where make install actually wrote; or
   • bootstrap with PREFIX="$HOME/.idris2" so the install lands where the
     binary looks — note this removes the need for sudo.
3. Bump the cache key (the current entries are populated under the old,
   split-prefix layout and would otherwise be restored unchanged), and narrow
   the path: list to the single prefix that is actually used.
4. With that landed, delete the repair step from abi-codegen-drift.yml and
   confirm the gate still prints connectors emitted: 16 /
   files compared: 3 of 3 and is green. Deleting the step without
   re-measuring is not acceptable — the step is the only thing currently
   proving the artefacts are present.
5. verify-proofs.yml stays green throughout (all three jobs:
   idris2 --check, lake build, TLC model-check).

Not a blocker

Per the standing ruling, this is an issue rather than a merge blocker: #819
works around it correctly and cheaply, anchored on $(idris2 --libdir) rather
than a hard-coded path, so it is immune to whichever way this is resolved.

Refs #811, #817, #819

🤖 Generated with Claude Code

https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV