Fix/abi gate chez support - #859
Merged
Merged
Conversation
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
Second layer of the same omission, measured on #817's own run. The first fix copied `support/` as data, which cured the COMPILE-time error and exposed the RUN-time one: INTERNAL ERROR: Can't find data file chez/support.ss (compile) (while loading libidris2_support.so) cannot open shared object file: No such file or directory (run) `libidris2_support.so` is a BUILT C library, not a data file. The Chez backend copies it out of `<libdir>/lib/` into the executable's `_app` directory at link time, so a build missing it still exits 0 and the failure only appears when the binary is first run -- one step later, inside the comparison, where it reads as a drift failure. Repairing this file by file is what produced the second failure. This commit stops doing that and uses the Idris2 tree's own targets instead: make -C <src> support # builds the C library make -C <src> install-support PREFIX=<p> # installs lib/ AND support/ which is complete by construction. `support/c/Makefile`'s own install target writes both `${PREFIX}/idris2-${VERSION}/lib` and `.../support/c`, so nothing is left to enumerate by hand. It costs seconds: it builds `support/` only, never the compiler. Measured on the CI runner, not assumed: prefix is `/home/runner/.idris2` and is writable, so no sudo is involved; the cache hit was on the shared key `idris2-v0.7.0-Linux-2`, confirming the omission comes from the sharing and not from a cold cache. The assertion now covers BOTH artefacts. The previous one checked only the compile-time file, which is precisely why the run-time one got through. Also asserts on the CONSUMER's artefact: after the build, that `build/abi-gen/exec/hypatia-abi-gen_app/libidris2_support.so` exists. A check on the producer proves nothing about the consumer -- the recurring guard/consumer trap -- and here the producer check genuinely passed while the consumer was broken. `Gen.idr` gains `--help` / `-h` exiting 0, so the build step can smoke- test that the binary actually RUNS. Missing arguments still print usage and exit 1: an explicit request for help succeeding and a usage error failing are different outcomes, and conflating them would have forced the workflow into an `|| true`, which is indistinguishable from a masked failure. Generated output is unaffected -- the provenance stamp hashes `Types.idr`, not `Gen.idr` -- and regeneration was verified byte- identical against all three tracked targets. Verified locally before pushing: --help / -h rc=0 no args / one arg rc=1 regenerate + diff connectors emitted: 16, 3 of 3, 0 drifted mutant: hand-edit generated Zig 1 drifted -> RED mutant: swap wire ids 3<->4 in the live Types.idr, no regen 3 drifted -> RED mutant: empty output dir compared 0 of 3 -> RED on the denominator positive control (clean tree) 3 of 3, 0 drifted -> GREEN The swap-ids mutant is the one that matters: it proves the gate reads the normative source, not merely that the generated copies agree with each other. Refs #120 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV
Contributor
|
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 configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (3)
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. Comment |
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers