fix(ci): build Idris2 outside the checkout — main's proof gate is red - #53
Merged
Merged
Conversation
The Idris2 Proof gate failed on its own commit (run 29559473259) for a reason the gate got RIGHT: the build step ran `tar xzf` inside the checkout, extracting Idris2-0.7.0/ (hundreds of .idr under libs/, benchmark/, docs/) into the tree the gate sweeps. "Any .idr not in the manifest is an error" then fired on the compiler's own sources. Fix: build the toolchain in a mktemp dir outside the checkout, so the only .idr files the gate sees are this repo's. Also untrack src/interface/build/ttc/2025081600/** -- committed TTC caches built by a different Idris2 (build/ is already gitignored; these predated the rule). Not the CI cause (a genuine 0.7.0 build stamps ttc version 2023090800 and ignores a 2025081600 cache), but build output never belongs in git. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.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.
What
Make main's Idris2 Proof gate pass. It is red on main right now (run on merge commit
91b16104= failure).Why main went red
PR #52 merged the sound gate but with a broken toolchain step. The workflow's "Build & install Idris2" ran
tar xzfinside the checkout, extractingIdris2-0.7.0/— which ships hundreds of.idrfiles underlibs/,benchmark/,docs/— into the very tree the gate sweeps. The gate's rule "any.idrnot in the manifest is an error" then fired on the compiler's own sources. Verified from the run-29559473259 log:FAIL: Idris2 modules present on disk but absent from the MANIFEST → Idris2-0.7.0/libs/base/....The gate did exactly what it should. The workflow was polluting the tree it scanned.
Fix
mktemp -doutside the checkout, so the only.idrthe gate sees are this repo's.src/interface/build/ttc/2025081600/**— committed TTC caches (build/is already gitignored; these predate the rule). Not the CI cause — a genuine 0.7.0 build stamps ttc version2023090800and ignores a2025081600cache — but build output never belongs in git.This is the fix for a gate that merged red once already (#52), and #51's real fix was likewise orphaned by a fast merge. Please let the check complete. Consider making Idris2 Proof a required status check so a red gate can't ride into main again.
🤖 Generated with Claude Code