fix(ci): call idris2 by full path before it is on PATH (required gate red since #820) - #880
Merged
Merged
Conversation
… red since #820) #820 moved `make install` from /usr/local (already on PATH) to $HOME/.idris2, but left `idris2 --version` as the last line of the SAME step, before the "Put Idris 2 on PATH" step runs. Every uncached run dies there with exit 127 ("idris2: command not found"). abi-codegen-drift is a REQUIRED status check on main, so this has held every hypatia PR since (main runs red 09-27, 09-28, 09-29). verify-proofs carries the identical line and is fixed the same way. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136eszqrQ53Kj7aBH1D4rXK
Contributor
|
Warning Review limit reachedNext included review available in 34 minutes. View limit detailsLimit details: You’ve used the included review currently available. You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Review configuration: ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (2)
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 |
hyperpolymath
enabled auto-merge (squash)
September 30, 2026 09:59
hyperpolymath
added a commit
to hyperpolymath/cicd-squabbler
that referenced
this pull request
Sep 30, 2026
The base gate feeds only the evidence-free listing once a PR is merged or closed, never an agent item; pinned by a new core test (killed by a mutant that routes every state through the open-PR path). Skipping the call keeps the commonest done-claim off the REST secondary limit this PAT shares with every other session -- live, 'landed hyperpolymath/hypatia#880' failed closed on exactly that 403. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136eszqrQ53Kj7aBH1D4rXK
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
The required check
abi-codegen-drifthas failed on every uncached run since #820. Main was red on 09-27, 09-28 and 09-29, and #876/#877 are both stuck on it. The cause:#820 moved
make installtoPREFIX="$HOME/.idris2", but the same step still ends with a bareidris2 --version.$HOME/.idris2/binonly joins$GITHUB_PATHin the next step. The fix calls the binary by its full path.verify-proofs.ymlhas the identical line and gets the same one-line fix.Why it matters
abi-codegen-driftis one of main's two required contexts, so while it is red no hypatia PR can merge. That includes #876, which restores compilation after #862. Every Hypatia scan in the estate is failing until #876 lands.Verification
This PR's own
abi-codegen-driftrun is the control. It either gets pastBuild Idris 2 from sourceor it doesn't.🤖 Generated with Claude Code
https://claude.ai/code/session_0136eszqrQ53Kj7aBH1D4rXK