Repository navigation
ci(kernel-proofs): Agda 2.6.4.3 and the PROOF-POLICY §2.1 invocation - #285
Conversation
The kernel-proofs job runs in debian:trixie-slim with agda-bin=2.6.4.3-1+b2, the prover resource-algebra, occupancy-types and choreographic-types pin in their own CI, so this gate re-checks their proofs on the same Agda instead of Ubuntu 24.04's 2.6.3. Idris2 0.8.0 is still built from source at its pinned commit; Debian names the Chez binary chezscheme, so the build finds whichever is present. tools/check-kernel-proofs.sh requires Agda 2.6.4.3, runs its own Agda checks under --safe --without-K --cubical-compatible, and sets LC_ALL=C.UTF-8: without a UTF-8 locale Agda stops with exit 42 on the Unicode warnings --cubical-compatible prints. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
|
Caution Review failedThe pull request is closed.
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. |
|
Secret Scanner, Governance and Hypatia Security Scan fail on this PR, but not because of it. They end in The fix is typed-wasm#284, which re-pins those reusables. It is blocked on a repository Actions setting; the comment there explains why. Once #284 lands, a merge from Everything this PR changes is green. Grade kernel proofs ran on Agda 2.6.4.3 with Generated by Claude Code |
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. |
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
|
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| # tools/check-kernel-proofs.sh refuses any other Agda. Until 2026-11-09 | ||
| # this job ran Ubuntu 24.04's Agda 2.6.3. | ||
| runs-on: ubuntu-latest | ||
| container: debian:trixie-slim |
Summary
The kernel-proofs gate re-checks the sibling repositories' Agda proofs (resource-algebra, occupancy-types, choreographic-types' K-CUT slice) and checks the kernel transcription table. It ran them on Ubuntu 24.04's Agda 2.6.3. Each sibling pins Agda 2.6.4.3 in its own CI, so this gate checked their proofs on a different prover.
The gate's own Agda checks also ran without
--cubical-compatible, the canonical theory invocation in PROOF-POLICY §2.1 (metadatastician/standards,3-practice/PROOF-POLICY.adoc).Changes
.github/workflows/contract-gate.yml(kernel-proofsjob):debian:trixie-slimwithagda-bin=2.6.4.3-1+b2, and asserts the version, as the siblings'proofs.ymldo.chezscheme, so the build uses whichever ofchezschemeandschemeexists.tools/check-kernel-proofs.sh:ALLOW_ANY_AGDA=1still overrides.--safe --without-K --cubical-compatible.LC_ALL=C.UTF-8. Without a UTF-8 locale, Agda stops with exit 42 on the Unicode warnings--cubical-compatibleprints.CHANGELOG.adoc: entry added.Not changed: the sibling pins. The siblings' own scripts run at those pins with their own flags. resource-algebra#19 and occupancy-types#18 move those scripts to the canonical flags. A later re-pin here picks them up, together with the stale
af95728citations.RSR Quality Checklist
Required
believe_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
CHANGELOGupdatedTesting
This environment cannot reach the Debian archive or Docker Hub, so it has no Agda 2.6.4.3. What I could check locally:
ALLOW_ANY_AGDA=1 bash tools/check-kernel-proofs.shgivesOK: kernel proofs — build, 13 rejection(s), table, and 4 negative control row(s).FAIL: Agda 2.6.4.3 required ....yqparses the workflow.The run that counts is this PR's
Grade kernel proofs (Idris2 0.8.0 + Agda)job, which is the first run on 2.6.4.3.CI note:
scan / gitleaksand the governance, Hypatia and mirror workflows fail on main too, until #284 lands.Generated by Claude Code