ci(abi): typecheck the Idris2 ABI in CI (G34)#52
Merged
Conversation
The ABI-FFI gate did a Julia structural conformance check and a Zig FFI build, but nothing ever ran idris2 on the ABI itself — so the 8 proof modules (Types, Layout, Foreign, Proofs, Semantics, Invariants, FfiSeam, Capstone) were authored and locally verified against Idris2 0.7.0 but never compiler-checked in CI. A future edit could break a proof and the gate would stay green. Adds an idris2-abi job running 'idris2 --typecheck julianiser-abi.ipkg' in the SHA-pinned stefan-hoeck/idris2-pack container (same image Axiom.jl uses), and uncomments idris2 0.7.0 in .tool-versions for local asdf use. Verified locally: both --build and --typecheck exit 0 on all 8 modules. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1
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
2 participants
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 the G34 hole: the ABI-FFI gate ran a Julia structural conformance check and a Zig FFI build, but nothing ever ran
idris2on the ABI itself. The 8 proof modules (Types,Layout,Foreign,Proofs,Semantics,Invariants,FfiSeam,Capstone— landed across PRs #38/#42/#43/#44/#45) were authored and locally verified against Idris2 0.7.0 but never compiler-checked in CI. A future edit could break a proof and the gate would stay green.Changes
.github/workflows/abi-ffi-gate.yml: newidris2-abijob runningidris2 --typecheck julianiser-abi.ipkgin the SHA-pinnedghcr.io/stefan-hoeck/idris2-packcontainer (the same prebuilt image theAxiom.jlidris2-abi-checkjob uses — avoids a ~10-min Chez/Idris2 source build). Header comment updated to describe all three jobs..tool-versions: uncommentidris2 0.7.0(pins the version the proofs were verified against, for localasdfuse). Nothing auto-installs from it, so this is documentation-only.RSR Quality Checklist
Required
idris2 --typecheck julianiser-abi.ipkgandidris2 --build julianiser-abi.ipkgboth exit 0 on all 8 modules (verified locally, Idris2 0.7.0).tool-versionsonly)believe_me/postulate/sorry) — the ABI modules are unchanged by this PR; the new job enforces their absence going forwardMPL-2.0header; no source files added).envfiles includedAs Applicable
src/interface/abi/on every push/PR; the existing structural + Zig jobs are untouchedTesting
Ground-truthed with Idris2 0.7.0:
cd src/interface/abi && idris2 --typecheck julianiser-abi.ipkg→ exit 0idris2 --build julianiser-abi.ipkg→ exit 0conformance,zig-build,idris2-abi;working-directorypathsrc/interface/abi/julianiser-abi.ipkgexists.The pinned container image is the identical digest already green in
Axiom.jl's equivalentidris2-abi-checkjob.🤖 Generated with Claude Code
https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1
Generated by Claude Code