fix(ci): install the Chez support tree so the ABI drift gate can pass by hyperpolymath · Pull Request #817 · hyperpolymath/hypatia

hyperpolymath · 2026-09-22T09:45:52Z

The gate I shipped in #811 is red on `main`

#811 merged with its own new ABI codegen drift check failing. This fixes it
forward. The gate is loudly red rather than silently green, so it is not a
vacuous gate — but a gate that has never passed is not yet evidence of
anything, and left red it trains people to ignore it.

The cause, measured

INTERNAL ERROR: Can't find data file chez/support.ss in any of
["/home/runner/.idris2/idris2-0.7.0/support/chez/support.ss",
 ".../base-0.7.0/data/chez/support.ss",
 .../contrib-0.7.0/data/chez/support.ss"]

Compiling an Idris2 executable needs the Chez support tree at
$(idris2 --libdir)/support/chez/support.ss. Type-checking and building a
library does not.

verify-proofs.yml only ever does the latter — idris2 --check over the proof
files, idris2 --build on two library packages — and never links a binary. So
the cache this job deliberately shares with it (same key
idris2-${IDRIS2_VERSION}-${runner.os}-2, chosen so the gate would not repeat
a 20-minute bootstrap) was populated without that tree.

Sharing a warm cache imports its omissions as well as its contents. That is
the generalisable lesson here, and it is why my local build passed while CI's
failed: locally the support tree exists under pack, so the local success was
never evidence about CI.

The fix

A step between "Verify Idris is on PATH" and "Build the generator" that:

resolves $(idris2 --libdir)/support and checks for chez/support.ss;
if absent, shallow-clones the Idris2 source at the pinned IDRIS2_VERSION
and copies support/ into place — support/ is plain data (Scheme and C
sources), needs no build, so this costs seconds, not a bootstrap;
asserts the file is present by name before continuing.

Step 3 matters independently of step 2. A missing support tree previously
surfaced as an opaque INTERNAL ERROR three steps later, inside the generator
build, where it read like a generator bug. Now it fails where it is caused.

Also in this PR

zig.yml extracted the test count with grep … || true, which the Hypatia
workflow scanner flagged at zig.yml:99 as swallowing a non-zero exit.

set -o pipefail already made a genuine zig test failure fatal, so nothing
was actually masked — but a suppressed exit code is indistinguishable from a
masked failure to a reader or a scanner, so this is a rewrite rather than an
argument. grep exits 1 on no-match, which under set -e needs suppressing;
awk exits 0 whether or not it matched, so the no-match case needs no
suppression at all and the count check below it becomes the only thing that can
fail the step.

Measured, not assumed — the extraction was run against the real zig test
output and three mutant logs:

Input	Extracted	Gate
real run (`All 4 tests passed.`)	`4`	green
`All 0 tests passed.`	`0`	red
no summary line at all	`0`	red
empty log	`0`	red
`3 of 7 tests passed.`	`7`	green

awk returns rc=0 on the no-match cases, which is the whole point of the
change.

The one remaining || true in abi-codegen-drift.yml — a diagnostic find
inside an already-failing branch — is replaced by a [ -d ] guard for the same
reason. There is now no || true in either workflow.

Not caused by this change

governance / Actions lockfile verify is red on every PR because #810 bumped 7
actions without refreshing .github/workflows/actions.lock
(taiki-e/install-action v2.87.13→v2.87.15, ruby/setup-ruby v1.323.0→v1.324.0,
docker/setup-buildx-action v4.4.0→v4.4.1, and a github/codeql-action SHA).
Every finding is on a workflow this PR does not touch. Filed separately —
folding an unrelated repo-wide fault into this PR would make both harder to
review.

The Check / Test / Clippy / Cargo check + clippy + fmt reds are
pre-existing on main (the unsatisfiable testcontainers constraint, #814),
as are the three governance / reds.

Acceptance

This PR is not done when it is merged; it is done when abi-codegen-drift
reports jobs > 0 and prints its denominator:

connectors emitted: 16
files compared:     3 of 3

Refs #120

🤖 Generated with Claude Code

https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV

The gate added in #811 failed on its own pull request and is now red on main. The failure is real and the cause is measured, not supposed: INTERNAL ERROR: Can't find data file chez/support.ss in any of ["/home/runner/.idris2/idris2-0.7.0/support/chez/support.ss", ...] Compiling an Idris2 EXECUTABLE needs the Chez support tree at `$(idris2 --libdir)/support/chez/support.ss`; type-checking and building a LIBRARY does not. `verify-proofs.yml` only ever does the latter -- it runs `idris2 --check` and `idris2 --build` on library packages and never links a binary -- so the cache this job deliberately shares with it (same key `idris2-${IDRIS2_VERSION}-${runner.os}-2`) was populated without that tree. Sharing a warm cache imports its omissions as well as its contents. `support/` is plain data (Scheme and C sources shipped in the Idris2 repo). It needs no build, so a shallow clone at the pinned tag repairs it in seconds rather than repeating the ~20-minute bootstrap. The new step then asserts the file is present BY NAME. Previously a missing support tree surfaced as an opaque INTERNAL ERROR three steps later, inside the generator build, where it read like a generator bug. Also in this commit: `zig.yml` extracted the test count with `grep ... || true`, which the Hypatia workflow scanner flagged at zig.yml:99 as swallowing a non-zero exit. `set -o pipefail` already made a genuine `zig test` failure fatal, so nothing was actually masked -- but a suppressed exit code is indistinguishable from a masked failure to a reader or a scanner, so the extraction is rewritten in awk, which exits 0 whether or not it matched and therefore needs no suppression at all. The count check below it is now the only thing that can fail the step. Measured against the real `zig test` output (4) and against three mutant logs (all 0, all red). The last `|| true` in abi-codegen-drift.yml -- a diagnostic `find` inside an already-failing branch -- is replaced by a `[ -d ]` guard for the same reason. Not addressed here, and not caused by this change: `governance / Actions lockfile verify` is red because #810 bumped 7 actions without refreshing `.github/workflows/actions.lock`. Filed separately. Refs #120 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV

coderabbitai · 2026-09-22T09:46:08Z

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: ca5d0508-412d-48dc-97ad-fe69db93d3c1

📥 Commits

Reviewing files that changed from the base of the PR and between e0393c2 and c82e9aa.

📒 Files selected for processing (2)

.github/workflows/abi-codegen-drift.yml
.github/workflows/zig.yml

 ________________________________
< I bench-press race conditions. >
 --------------------------------
  \
   \   \
        \ /\
        ( )
      .( 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

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

… pass (#819) ## 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: ```sh 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.com/claude-code) https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

hyperpolymath mentioned this pull request Sep 22, 2026

feat(abi): generate the Zig and Rust wire enums from the normative Idris2 ABI (#120) #811

Merged

hyperpolymath merged commit 5060161 into main Sep 22, 2026
35 of 45 checks passed

hyperpolymath deleted the fix/abi-gate-chez-support branch September 22, 2026 09:46

This was referenced Sep 22, 2026

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

Merged

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

Closed

This was referenced Sep 22, 2026

abi: generate the Zig and Rust wire enums from the normative Idris2 ABI metadatastician/IDApTIK#120

Closed

policy: implement Idris2 ABI, Zig FFI, and Hexadeca conformance metadatastician/IDApTIK#103

Closed

Navigation Menu

Repository navigation

fix(ci): install the Chez support tree so the ABI drift gate can pass - #817

fix(ci): install the Chez support tree so the ABI drift gate can pass#817
hyperpolymath merged 1 commit into
mainfrom
fix/abi-gate-chez-support

hyperpolymath commented Sep 22, 2026

Uh oh!

coderabbitai Bot commented Sep 22, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented Sep 22, 2026

The gate I shipped in #811 is red on main

The cause, measured

The fix

Also in this PR

Not caused by this change

Acceptance

Uh oh!

coderabbitai Bot commented Sep 22, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

The gate I shipped in #811 is red on `main`