Repository navigation
ci(kernel-proofs): pin the runner and require Agda 2.6.3 - #280
Conversation
ubuntu-latest moved to Ubuntu 26.04 on 2026-10-19. The kernel-proofs job installs Agda from apt, so it got Agda 2.8.0, which prints error locations as file:11.38 where 2.6.3 printed file:11,38. occupancy-types' own reject check only accepts the old form, so it reported CostIsOccupancy as an unexpected failure even though Agda refused it correctly. Every PR now fails the job; main last ran it on 2026-10-17, before the move. The job runs on ubuntu-24.04, whose agda-bin is 2.6.3, and check-kernel-proofs.sh refuses any other Agda (ALLOW_ANY_AGDA=1 to override), as it already refuses any Idris2 but 0.8.0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
|
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 10 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. Comment |
SonarCloud (shell rule: prefer [[ over [) on the line added in 1b98e5d. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
|
Add Carrot credits or activate Agent usage billing to use Autofix |
Codex Review SummaryThis 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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1e4944afef
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
The glob *"version 2.6.3"* also accepted 2.6.3.1 or 2.6.30. The check now requires the line to be exactly "Agda version 2.6.3". Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
|
|
The required The fix is the estate re-pin of the standards reusables to Generated by Claude Code |
Summary
The Contract Gate's "Grade kernel proofs (Idris2 0.8.0 + Agda)" job now fails on every PR, for a reason no PR introduced.
On 2026-10-19,
ubuntu-latestmoved to Ubuntu 26.04. The job installs Agda from apt, so it now gets Agda 2.8.0 (the log showsImage: ubuntu-26.04andAgda version 2.8.0). Agda 2.8.0 prints error locations asCostIsOccupancy.agda:11.38-42, where 2.6.3 printed:11,38. occupancy-types' ownscripts/check-agda.shaccepts only[0-9]+,[0-9]+, so it reports a correct rejection asERROR: unexpected failure while checking CostIsOccupancy. Main last ran this job on 2026-10-17, before the move, and it passed.It first showed up on #279 (run 40415000878).
Changes
.github/workflows/contract-gate.yml: the kernel-proofs job runs onubuntu-24.04, whoseagda-binis 2.6.3. The other two jobs are toolchain-free and stay onubuntu-latest.tools/check-kernel-proofs.sh: refuses any Agda other than 2.6.3, unlessALLOW_ANY_AGDA=1is set. It already refuses any Idris2 other than 0.8.0. With this check, the next image change fails with a clear message instead of an opaque reject failure.CHANGELOG.adocentry.Not in this PR: occupancy-types' location regex could accept both formats. That would be an upstream change in occupancy-types and a re-pin here. The version check makes this repo correct either way.
RSR Quality Checklist
Required
.envfiles includedAs Applicable
CHANGELOGupdatedTesting
Run locally on Ubuntu 24.04.5 with
agda-bin2.6.3-1build1:tools/check-kernel-proofs.shprintsOK: kernel proofs — build, 11 rejection(s), table, and 4 negative control row(s).agdareportingAgda version 2.8.0first onPATH, it printsFAIL: Agda 2.6.3 required …and exits 1.Generated by Claude Code