lean 4.35.0 + aeneas-latest → upstream Lean-4.35 (aeneas fdebf20d) by bryan-minimal · Pull Request #1000 · gominimal/pkgs

bryan-minimal · 2026-10-23T02:43:49Z

lean 4.34.1 → 4.35.0, together with aeneas-latest moved to upstream AeneasVerif/aeneas main at fdebf20d (2026-10-22), whose backends/lean/lean-toolchain is leanprover/lean4:v4.35.0. Split out of #999.

Why these two move together

#999 bumped lean on its own and its minimal build failed (run d4401ce3). aeneas-latest failed on both arches about five seconds into its lake build:

✖ [16/41] Building Cache.Requests
error: Cache/Requests.lean:988:2: Missing cases:
(Lake.PackageEntrySrc.path _ true)

Lean 4.35's Lake gave PackageEntrySrc.path an extra field, so the September Mathlib pin (d13f23b7, built for 4.34) no longer compiles its own cache tool. Mathlib's tooling is compiled against the running Lean, so a Mathlib pinned for one Lean minor doesn't build on the next. Upstream aeneas moved to v4.35.0 in AeneasVerif/aeneas#1448, so this PR tracks it instead of porting again.

What changed

lean: 4.35.0, with the same version and sha256 as Update stacked: 5 packages #999 (6747b099…c307b).
aeneas-latest: version 20261022, source aeneas-fdebf20, and upstream's lake-manifest.json taken verbatim. Every Lake dependency is re-pinned from it:

dep	old	new
mathlib4	`d13f23b7`	`56a00585` (tag v4.35.0)
plausible	`118aa17e`	`dfa4f381`
LeanSearchClient	`ddf04cf3`	`d6b4c7be`
import-graph	`e928b725`	`a41f0e9a`
ProofWidgets4	`106ff4fa`	`df72b022`
aesop	`355695d5`	`4a174c49`
quote4 (Qq)	`6a489d9a`	`dce0ad79`
batteries	`f2effa3d`	`66e46918`
lean4-cli	`e92c9f15`	`c24fe607` (tag v4.35.0)

Each tarball is GitHub's archive of that commit, mirrored no-clobber to gs://minimal-staging-archives/aeneas-latest/. The sha256 read back from GCS matches the download for all ten.
The 4.34 port patch (aeneas-lean-4.34.patch) is deleted. Upstream targets the Lean we ship, so nothing needs porting. The patch build dep goes with it.
A new guard in build.sh: it refuses to build if aeneas's lean-toolchain stops naming the lean we ship, with "bump lean and aeneas-latest together". So a future lone lean bump fails with that message instead of a Mathlib pattern-match error.
Mathlib cache closure: 28 → 31 modules (Data.Int.GCD, Data.List.Monad and Order.FixedPoints are new), recomputed from every import Mathlib… under Aeneas/ and AeneasMeta/.

Translator (`aeneas` package): unchanged, on purpose

Upstream's library is now a Lean module (Aeneas.lean begins module / public import …). The translator we ship, d119a47, defaults to non-module output (import Aeneas, see aeneas/build.sh use_lean_modules). That was the fix for the opposite direction: a module file can't import a non-module library. A plain file importing a module library is allowed, and the imports_aeneas test exercises exactly that.

Bumping the translator is the charon / rust-nightly cascade (pkgmgr bundle-bump aeneas), so it stays a separate PR.

Verification

nickel format --check, bash -n and MINIMAL_SCIENCE_MODE=1 mip dump --packages (amd64 + arm64) are clean.
Blast radius: exactly 2 spec hashes change, lean and aeneas-latest.
Remote session: --rebuild lean and aeneas-latest, then min check. Results are posted below once they finish.

Follow-up for pkgmgr (not changed here)

pkgmgr-rs#1046's toolchain pre-flight (data/toolchain_constraints.toml) should learn a consumer-compat rule, so the bot never opens a lone lean bump again. The rule: a lean bump to X requires aeneas-latest's pinned backends/lean/lean-toolchain to equal leanprover/lean4:vX in the same run; otherwise drop lean with "did NOT ship: aeneas-latest targets lean Y". That needs a constraint keyed on a dependent package's pinned file, not just a toolchain version. Today the table only covers "X needs toolchain ≥ Y".

🤖 Generated with Claude Code

Summary by CodeRabbit

Updates
- Updated the bundled Lean toolchain to version 4.35.0 and aligned the Aeneas version with it.
- Refreshed supporting libraries and dependencies to versions compatible with the updated toolchain.
- Expanded the set of Mathlib modules available in the build cache.

lean 4.35.0 broke aeneas-latest's Sept Mathlib pin (Lake's PackageEntrySrc.path gained a field; mathlib Cache/Requests.lean:988 "Missing cases"), failing pkgs#999's run d4401ce3. Upstream aeneas moved to Lean v4.35.0 (#1448), so track main at fdebf20d with its own lake-manifest: mathlib v4.35.0 (56a00585) and every Lake dep re-pinned and mirrored. The 4.34 port patch is dropped (upstream targets the Lean we ship); build.sh now refuses to build if aeneas's lean-toolchain stops matching our lean. Mathlib cache closure 28 -> 31 modules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

coderabbitai · 2026-10-23T02:44:07Z

Warning

Review limit reached

Run on-demand review

_{This review includes 1 billable file and costs up to $0.25.}

Ask an admin to make reviews automatic

Open in CodeRabbit

Reviews can continue after your included limit without a manual trigger. An admin must approve usage-based billing.

Or wait 32 minutes for your next included review.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available. Your 68 included PR review attempts over the past 7 days set your current allowance at 1 review per hour.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Source mode: Auto
Repository: gominimal/pkgs
Branch: lean-4.35-aeneas-latest
File: .coderabbit.yaml
Commit: 12191e1
Layers: Repository YAML
Review profile: CHILL
Plan: Essentials
Run ID: 97c51366-b152-44f4-a9b9-511d0a5cb069

📥 Commits

Reviewing files that changed from the base of the PR and between ebbc5c3 and 12191e1.

📒 Files selected for processing: 1

packages/aeneas-latest/build.ncl

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Source mode: Auto
Repository: gominimal/pkgs
Branch: lean-4.35-aeneas-latest
File: .coderabbit.yaml
Commit: ebbc5c3
Layers: Repository YAML
Review profile: CHILL
Plan: Essentials
Run ID: 5d02dbbd-7ad1-4596-a3a2-b7140d22a523

📥 Commits

Reviewing files that changed from the base of the PR and between 30ab8a3 and ebbc5c3.

📒 Files selected for processing: 5

packages/aeneas-latest/aeneas-lean-4.34.patch
packages/aeneas-latest/build.ncl
packages/aeneas-latest/build.sh
packages/aeneas-latest/lake-manifest.json
packages/lean/build.ncl

💤 Files with no reviewable changes: 1

packages/aeneas-latest/aeneas-lean-4.34.patch

Included review availability: This review used your included allowance. 0 included reviews remain after this review. Your included PR review attempts over the past 7 days set your current allowance at 1 review per hour.

📝 Walkthrough

Aeneas now uses an updated upstream revision and Lean 4.35.0 without the local Lean 4.34 compatibility patch. The build checks the vendored Lean version and updates its pinned dependencies and Mathlib cache inputs. The translator package remains unchanged.

Changes: Aeneas and Lean toolchain update

Layer / File(s)	Summary
Update the Lean and Aeneas build baseline `packages/lean/build.ncl`, `packages/aeneas-latest/build.ncl`, `packages/aeneas-latest/aeneas-lean-4.34.patch`, `packages/aeneas-latest/build.sh`	The Lean package moves to 4.35.0, and Aeneas tracks a newer revision without the local Lean 4.34 compatibility patch. The build checks that the vendored Lean version matches the shipped version.
Update dependency pins and cache inputs `packages/aeneas-latest/lake-manifest.json`, `packages/aeneas-latest/build.ncl`, `packages/aeneas-latest/build.sh`	The Lake manifest and vendored dependency sources use updated revisions. The Mathlib cache request adds `Mathlib.Data.Int.GCD`, `Mathlib.Data.List.Monad`, and `Mathlib.Order.FixedPoints`.

Priority: ⬇️ Low

Estimated code review effort: 3 (Moderate) | ~20 minutes

Change: Other

Suggested reviewers: 0chroma

Merge Risk: ⚪ Minimal · up to ebbc5

No actionable merge-blocking issue was found. The reported rebuild and package checks remain to be confirmed as part of normal validation.

Pre-merge checks: 5

Check name	Status	Explanation
Description Check		Check skipped - CodeRabbit’s high-level summary is enabled.
Title check		The title clearly identifies the Lean 4.35.0 update and the aeneas-latest move to upstream Aeneas commit fdebf20d, which are the main changes.
Docstring Coverage		No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 1…
Linked Issues check		Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check		Check skipped because no linked issues were found for this pull request.

Full details: Docstring Coverage

Explanation

No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 1 files. (3 skipped: 3 unsupported.)

✨ Finishing Touches

📝 Generate docstrings

Commit to this branch
Create a new PR

🧪 Generate unit tests (beta)

Commit to this branch
Create a new PR

Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

_{Comment @coderabbitai help to get the list of available commands.}

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

bryan-minimal · 2026-10-23T03:11:18Z

Remote session verification on head ebbc5c31, built with --rebuild in a fresh session (lean435, now destroyed). The later commit 12191e11 only changes a comment, and the spec hash is the same: aeneas-latest 164f5879… before and after.

lean 4.35.0: a real from-source build (8.5k log lines ending Built target stage1).
aeneas-latest:
- the new toolchain guard passed, since lean-toolchain = leanprover/lean4:v4.35.0 matches the lean we ship;
- lake exe cache get fetched the 31-module Mathlib closure, 1,474 files;
- lake build Aeneas ended Build completed successfully (1760 jobs) with no patch applied;
- the build log has 0 declaration uses 'sorry' warnings.
min check --packages lean aeneas-latest: every check passes on both packages, including standalone tests (lean's #eval, and aeneas-latest's imports_aeneas). No Skip. The latter is a non-module file doing import Aeneas from the now module-based library, which is what the translator's default output does.

🤖 Generated with Claude Code

bryan-minimal requested a review from a team as a code owner October 23, 2026 02:43

bryan-minimal mentioned this pull request Oct 23, 2026

Update stacked: 5 packages #999

Merged

aeneas-latest: cache closure is 1,474 files at Mathlib v4.35.0 (comment)

12191e1

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

norrietaylor approved these changes Oct 23, 2026

View reviewed changes

bryan-minimal added this pull request to the merge queue Oct 23, 2026

Merged via the queue into main with commit d9ce3d2 Oct 23, 2026
11 checks passed

bryan-minimal deleted the lean-4.35-aeneas-latest branch October 23, 2026 22:39

Navigation Menu

Repository navigation

lean 4.35.0 + aeneas-latest → upstream Lean-4.35 (aeneas fdebf20d) - #1000

lean 4.35.0 + aeneas-latest → upstream Lean-4.35 (aeneas fdebf20d)#1000
bryan-minimal merged 2 commits into
mainfrom
lean-4.35-aeneas-latest

Uh oh!

Review limit reached

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Uh oh!

Why these two move together

What changed

Translator (aeneas package): unchanged, on purpose

Verification

Follow-up for pkgmgr (not changed here)

Summary by CodeRabbit

Uh oh!

Uh oh!

Review limit reached

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Translator (`aeneas` package): unchanged, on purpose