chore: migrate to Lean 4.31 - #2208
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_19f7579d-19ce-4e3d-820a-1962ff5b76c3) |
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟢 No findings from the OCR first pass. Advisory only.
No comments generated. Looks good to me.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: small-lean (router-v10)
- Changed files: 2 supported / 3 total; Lean 1, trust docs 0, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 35 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 3; tokens 38986; tool calls 5; warnings 0; duration 76s
- Largest changed files: lake-manifest.json (+17/-16), lakefile.lean (+1/-1)
Pilot mode: advisory only. Codex Review remains the merge gate.
![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: 9232f95d7a
ℹ️ 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".
| "subDir": null, | ||
| "scope": "", | ||
| "rev": "38d53df8b4488d5322894619ea8385fcbb2e6f5d", | ||
| "rev": "f7e4ee0dc8f8d5265ce822a937ab5be771f182e9", |
There was a problem hiding this comment.
With the root manifest pinned to this SHA, python3 scripts/generate_evmyullean_fork_audit.py --check now aborts because the hand-maintained audit and artifacts/evmyullean_fork_audit.json still record 38d53df...; the same check also iterates the split-package manifests, which remain pinned to that old commit. Consequently the required fork-conformance check cannot pass and the published trust-boundary report describes a dependency revision that Verity no longer uses. Update the audit record/artifact and all split-package pins together with this root pin.
Useful? React with 👍 / 👎.
| @@ -1 +1 @@ | |||
| leanprover/lean4:v4.24.0 | |||
| leanprover/lean4:v4.31.0 | |||
There was a problem hiding this comment.
After changing this toolchain, artifacts/verification_status.json still reports leanprover/lean4:v4.24.0. Because collect_metrics() reads lean-toolchain, python3 scripts/generate_verification_status.py --check now exits with “Stale verification artifact,” which also makes a direct make check fail and exposes incorrect toolchain metadata to artifact consumers. Regenerate and commit the verification-status artifact as part of the migration.
Useful? React with 👍 / 👎.
1 participant
Summary
f7e4ee0dc8f8d5265ce822a937ab5be771f182e9Scope
Migration compatibility only; no proof or contract semantics were changed.
Validation
lake build Verity(receipt tracked separately)Note
Medium Risk
A multi-version Lean jump with a full transitive dependency repin can break builds or proofs until CI passes, though the PR scope is limited to toolchain files with no stated semantic changes.
Overview
Bumps the project from Lean 4.24.0 to Lean 4.31.0 via
lean-toolchainand refreshes the Lake lockfile (manifest 1.2.0, includingfixedToolchain: false).EVMYulLean is repinned in
lakefile.leantof7e4ee0dc8f8d5265ce822a937ab5be771f182e9for the 4.31-compatible graph. Transitive pins move with it—notably mathlib tov4.31.0and refreshed revs for ProofWidgets4, Cli, batteries, aesop, and other inherited packages.No application Lean sources appear in the diff; this is toolchain and dependency alignment only.
Reviewed by Cursor Bugbot for commit 9232f95. Bugbot is set up for automated code reviews on this repo. Configure here.