Repository navigation
aeneas chain → 2026-10-30: aeneas ab34bd2, charon 0.1.304, aeneas-latest ab34bd2, nightly 2026-09-17 (unchanged) - #1271
Conversation
…nightly 2026-09-17 unchanged) aeneas upstream HEAD (2026-10-30) pins charon 7b462d9 = 0.1.304 via its charon-pin; charon and charon-ml follow that pin, not charon's newest release. charon 0.1.304's rust-toolchain is still nightly-2026-09-17, so rust-nightly-charon does not move. Crates re-vendored (338 crates, the same two git forks). Generated by `pkgmgr bundle-bump aeneas charon charon-ml` (Cloud Build 73c3c070); stale pin comments fixed by hand. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
No actionable comments were generated in the recent review.
 |
| Layer / File(s) | Summary |
|---|---|
Update Aeneas source pins packages/aeneas-latest/build.ncl, packages/aeneas-latest/build.sh, packages/aeneas/build.ncl |
Both Aeneas packages use commit ab34bd2 and matching source archive metadata. The aeneas-latest build script enters the updated checkout directory. |
Update Charon sources and build inputs packages/charon/build.ncl, packages/charon/build.sh, packages/charon-ml/build.ncl |
Charon and charon-ml use version 0.1.304 with updated source and vendor archive metadata. The Charon build extracts the pinned minirust archive and checks for tooling/miniutil/src/lib.rs. |
Estimated code review effort: 2 (Simple) | ~10 minutes
Possibly related PRs
- gominimal/pkgs#1000: Updated
aeneas-latestto the prior Aeneas revision and Lean 4.35. - gominimal/pkgs#1132: Added a TLS-stack guard to the Charon build script.
Suggested reviewers: norrietaylor, mitodrummer
Merge Risk: 
404dc
-
No actionable merge-blocking risk is established; proceed with normal build validation.
Pre-merge checks: 
-
Check name Status Explanation Description Check Check skipped - CodeRabbit’s high-level summary is enabled. Title check The title names the main change: moving the aeneas and charon chain to new pins (aeneas ab34bd2, charon 0.1.304, aeneas-latest ab34bd2) with the nightly unchanged. The diff matches these pins. The tit… Docstring Coverage No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat… 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: Title check
-
Explanation
The title names the main change: moving the aeneas and charon chain to new pins (aeneas ab34bd2, charon 0.1.304, aeneas-latest ab34bd2) with the nightly unchanged. The diff matches these pins. The title is long and lists several pins, but it is accurate and specific enough for a reviewer scanning history.
Full details: Docstring Coverage
-
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 2 files. (4 skipped: 4 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
…rust` feature needs it)
charon 75b7a1c ("Use miniutil", after 0.1.281) added crates/miniutil, whose
lib path is the crates/minirust submodule's tooling/miniutil/src. GitHub's
archive omits submodules, so 0.1.304 failed with "couldn't find file
.../minirust/tooling/miniutil/src/lib.rs". Pin the gitlink commit
(Nadrieril/minirust c0b555e, mirrored create-only) as its own Source and
extract it into crates/minirust, keeping upstream's default features.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ith the translator The translator at ab34bd2 maps slice::Iter's DoubleEndedIterator::next_back to `core.slice.iter.IteratorSliceIter.next_back` (upstream #1386), which the fdebf20 library lacks: a model of `v.iter().rev()` failed in lean with "Unknown identifier". Same Lean (4.35.0) and byte-identical lake-manifest.json, so only the aeneas source moves; mirrored create-only (same bytes as aeneas-20261030.tar.gz). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
There was a problem hiding this comment.
Reviewed at 404dc1a: aeneas/charon/minirust sha256s match upstream codeload; charon-pin, flake.lock, rust-toolchain (nightly-2026-09-17) and lake-manifest all consistent with the pins; build.sh changes (minirust submodule extraction) correct and offline. Low note: nothing ties the minirust tarball pin to charon's gitlink, so a stale pin on a future bump would pass the test -f check — agree with the proposed pkgmgr follow-up. Did not verify gs:// mirrors or the vendor tarball sha (gcloud auth).
aeneas chain → 2026-10-30: aeneas ab34bd2, charon/charon-ml 0.1.304, aeneas-latest ab34bd2; nightly 2026-09-17 unchanged
The fv-lab Rust→Lean translator was three weeks behind upstream. aeneas HEAD (2 8000 026-10-30, ab34bd2) pins charon 7b462d9, which is charon 0.1.304. We ship aeneas 2026-10-08 with charon/charon-ml 0.1.281 (the last chain bump was #843).
aeneascharon,charon-mlcharon-pinaeneas-latest(Lean library)rust-nightly-charonrust-toolchainis stillnightly-2026-09-17leanbackends/lean/lean-toolchainis stillv4.35.0charon follows aeneas's pin, not charon's newest release (0.1.307). aeneas is written against one charon commit, and its LLBC reader (charon-ml) must match the charon binary that wrote the file. Taking the newest charon would break that contract.
Commit 1: generated by
pkgmgr bundle-bump aeneas charon charon-mlThis ran from pkgmgr-rs main 0efae50 in Cloud Build
73c3c070-0638-4ab5-a362-0de3716c4d24, against pkgs main 8f25b19.What the tool did:
ls-remote;Nadrieril/specr?branch=bump-toolchainandNadrieril/tracing-tree, so thebuild.shvendor block is unchanged apart from the tarball name;versionlets, shas andstrip_prefixes;.sha256. They hash identically to whatrust-nightly-charonalready pins, which is why that file has no diff.Done by hand: the date/version text in the header comments beside the new pins, which the tool flags for review.
Hand step 1: charon needs its
crates/minirustsubmodulecharon0.1.304 first failed to build:charon 75b7a1c ("Use miniutil", after 0.1.281) added
crates/miniutil, which is built by the defaultminirustfeature. Its[lib] pathpoints into thecrates/minirustgit submodule, and GitHub archives leave submodules out.The fix keeps upstream's default features:
c0b555e5b15accc6c1366b1d911a1bfd49c3d9d0(a fork of minirust/minirust on branchbump-toolchain, Apache-2.0 OR MIT), is pinned as its ownSourceand mirrored.build.shextracts it intocrates/minirustand checks thattooling/miniutil/src/lib.rsis there.Reviewer note: this pin is NOT bumped by
bundle-bump. On the next bump, re-checkgit ls-tree <charon commit> crates/minirust. A pkgmgr follow-up should teach the recipe about submodules.The alternative,
--no-default-features --features rustc, would build without the submodule, but it drops--format minirust/--run-with-minirust, which 0.1.281 shipped.Hand step 2: aeneas-latest moves with the translator
The translator at ab34bd2 maps
slice::Iter'sDoubleEndedIterator::next_backtocore.slice.iter.IteratorSliceIter.next_back(upstream #1386, which is what.iter().rev()reaches). The fdebf20 Lean library has no such definition.I reproduced the failure: with only commit 1 applied, a two-function crate using
v.iter().rev().next()translates, butleanrejects the model withUnknown identifier core.slice.iter.IteratorSliceIter.next_back. With aeneas-latest at ab34bd2 the same model type-checks. Control: the same crate withoutrev()type-checks against either library.Why the bump is safe:
lake-manifest.jsonat ab34bd2 is byte-identical topackages/aeneas-latest/lake-manifest.json(Mathlib 56a0058), so only the aeneas source moves.aeneas-20261030.tar.gz, mirrored a second time underaeneas-latest/.Target.leanaxioms becameopaque/defs, and twolakefileneedslines were added.The
use_lean_modules = ref falsedefault inaeneas/build.shstill holds: Config.ml still hasref true, and thegrep -qguard matches. The fv-smoke model (non-module output importing the module library) still checks.Mirrored objects
New objects in
gs://minimal-staging-archives. Each was copied create-only (cp -n) and its sha256 was re-checked after downloading it back:aeneas-20261030.tar.gzcbdf6ca6efc17a994172de6f2c284b3c86807601996da417a345a7791742061b(= codeload legacy tarball of ab34bd2)aeneas-latest/aeneas-ab34bd2.tar.gzcbdf6ca6efc17a994172de6f2c284b3c86807601996da417a345a7791742061b(same bytes)charon-ml-0.1.304.tar.gz445c1e303ccafc5ab5bbf14f2cddde48baaf2a281ba4093ee4e0b2a3dc4ab125(= codeload legacy tarball of 7b462d9)charon-vendor-0.1.304.tar.gza41e218c07104d90b12f8e2e3c71fa95a2cde26bc1a1a2d95d1155f6c43da346charon-minirust-c0b555e.tar.gz4380fe1dbde99cd50b6a452e07021f4474e8a7d290ffff7776f274cb78f952a4(GitHub tarball of Nadrieril/minirust c0b555e)The 9 nightly-2026-09-17 objects already existed, and their MD5s match the re-fetched,
.sha256-verified copies.aeneas
build.shnotescore_unixfromsrc/duneand removed theCore_unix.mkdir_p/Core.Fn.composeuses. The matchingseds are now no-ops. They are harmless, so they're left in to keep this PR mechanical; they can be removed later.progressanddomainslibstubs are still needed.aeneas.opam/dune-projectnow listcalendarandunionFind. Neither is insrc/dune'slibraries.Verified (Minimal sessions, arm64)
charon,charon-ml,aeneasandaeneas-latestall build with--rebuild --verbose(aeneas-latest: 1760 Lake jobs).min checkpasses every checker for all four packages, including the standalone tests.fv-smokepasses all 18 checks in a session on this branch, withcharon versionreporting 0.1.304. That includescharon + aeneas + lean: verify, the full loop: charon → aeneas →leanon the model →leanonProofs.lean.rev()model: type-checks against the new aeneas-latest. It fails without hand step 2, as described above.amd64: not verified locally; build-bot covers it.
🤖 Generated with Claude Code
Summary by CodeRabbit