Repository navigation
fix(abi): put the Eq doc comment above public export in Types.idr - #285
Conversation
The merge placed '||| Equality on severity' between 'public export' and 'Eq Severity where'. Idris2 then rejects 'public export' as a declaration start (idris-abi on b332b5f). Doc comment first, as on main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
|
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 56 minutes. View limit details
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. |
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
#277 merged at b332b5f. The fix for its one failing check (7070cb8) was pushed to the branch but did not land.
Problem
On main,
src/abi/Types.idrhas the|||doc comment betweenpublic exportandEq Severity where. Idris2 0.7.0 rejects it:So the required job "Idris2 ABI proofs type-check" fails on main and on every PR based on it (failing run).
Change
Move the doc line above
public export. One line, no change to any declaration.Verification
The same commit is on #277's branch. The other 4 modules passed in the failing run; this is the only error.
Generated by Claude Code