fix(test-proofs): make the Idris2 ABI check able to fail (P0-2)

[hyperpolymath]

ULTRAPLAN P0-2 — just test-proofs could never fail. Now it can.

Defect (Justfile:92-105 on 0613e69)

• $$f is not a just escape: bash received $$ (PID) + f, so every file printed [SKIP] … not found — the check examined nothing.
• A failed idris2 --check printed [FAIL] and continued; the recipe exited 0.
• Missing idris2 printed SKIP and exited 0.
• Checking the files individually could not work anyway: idris2 --check src/abi/Types.idr → Module name JanusKey.ABI.Types does not match file name.

Change

• test-proofs → bash shebang recipe, set -euo pipefail, runs idris2 --typecheck src/idris-abi/januskey-abi.ipkg. Missing idris2 = exit 1 unless ALLOW_NO_IDRIS=1 (explicit, loud SKIP).
• src/idris-abi/ — the ipkg plus relative symlinks into src/abi/ laid out by module path. The sources stay put because tests/aspect/cross_cutting_test.sh, the Mustfile and the Zig FFI name src/abi/<File>.idr; physically moving them belongs with J1-3.
• .github/workflows/idris-abi.yml — non-required job idris-abi (expected red until J1-3) in the same idris2-pack@sha256:f0758996… image pages.yml uses.

Evidence

Run	Result
local idris2 0.7.0, just test-proofs	rc=1 — 10 errors, all Types.idr (first: Undefined name isInfixOf, :63)
CI image locally (Idris 2, version 0.8.0-6ca00e72e)	rc=1, same 10 errors
idris2 absent from PATH	rc=1 FAIL: idris2 not installed…
idris2 absent, ALLOW_NO_IDRIS=1	rc=0 SKIP: … ABI proofs were NOT checked.
positive control: trivial package	rc=0
negative control: package naming a missing module	rc=1

This job is expected red. That is the honest state of the ABI proofs: they have not typechecked on main. J1-3 fixes them; the job then goes green and can be made required.

Known, deliberately not fixed here

• Foreign.idr declares Januskey.ABI.Foreign and imports Januskey.ABI.{Types,Layout} which no file declares; Proofs.idr imports JanusKey.ABI.Foreign. Casing fix = J1-3. (The Januskey/+JanusKey/ dirs collide on case-insensitive FS; noted in the ipkg.)
• test-all depends on test-proofs and is therefore red until J1-3 — correct.
• .machine_readable/contractiles/Justfile:91 keeps the old $$f recipe.
• actions.lock: not edited (no fix mode). --no-fix drift is pre-existing (4/22 before, 4/23 after: codeql-action, haskell-actions/setup, action-send-mail). Checkout is pinned by full SHA so the new workflow stands alone.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VxcAoyMQe7CjQwCKL18Mm4

[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: 62b16994-c42c-44c3-b337-dd1f9d870fee

📥 Commits

Reviewing files that changed from the base of the PR and between 0613e69 and a6227af.

📒 Files selected for processing (7)

• .github/workflows/idris-abi.yml
• Justfile
• src/idris-abi/JanusKey/ABI/Layout.idr
• src/idris-abi/JanusKey/ABI/Proofs.idr
• src/idris-abi/JanusKey/ABI/Types.idr
• src/idris-abi/Januskey/ABI/Foreign.idr
• src/idris-abi/januskey-abi.ipkg

 ___________________________
< Goodbye, pre-merge panic. >
 ---------------------------
  \
   \   (\__/)
       (•ㅅ•)
       / 　 づ

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Autopilot is currently an internal CodeRabbit preview.

---

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.}