[SwayamInSync]

Lean projects now pin leanprover/lean4:v4.35.0, the latest stable release (2026-10-12), instead of v4.32.2. Moving the pin also exposed two problems with how a project's toolchain is handled:

	main	Now
Certification under elan, whose default toolchain is not the pin	builds with elan's default: elan picks a toolchain by the working directory, not by lake --dir	every step names the pin: lake +leanprover/lean4:v4.35.0 --dir=DIR …
A lake outside elan that runs another Lean	certifies with it	refused: the project pins leanprover/lean4:v4.35.0, but /path/lake runs Lean 4.1.0; install elan …, which runs the pinned toolchain
A project 0.1 generated, pinned to v4.32.2	— (the pin did not move)	moved to the new pin with a warning
A project pinned to a toolchain no release wrote	error	error, as before

The first was hidden because CI installs the pin as elan's default. After this move, a machine whose default is still v4.32.2 would have built every project with 4.32.2.

The warning, on a 0.1 project:

warning: the Lean project proof pinned leanprover/lean4:v4.32.2, which an earlier release of cpp-verify wrote; it now pins leanprover/lean4:v4.35.0, so a proof that no longer builds needs updating for that Lean
Exported: lean obligation: trivial

Design

• One pin, and the pins that came before (Driver/CppVerifyVersion.h): LeanToolchain is the pin; EarlierLeanToolchains lists those earlier releases wrote. cpp-verify owns a project's lean-toolchain, since its generated semantics are written for one Lean. So a pin it wrote in an earlier release is its own to move, and the migration rewrites it once, with a warning. Any other pin is the user's, and stays an error. This is the toolchain part of the 0.1-project migration the plan bundles into 0.2; proof identity (LM3) migrates proof files later.
• Certification runs the pin: when lake is elan's proxy, every step is lake +<pin> --dir=DIR …, as elan run and lake +toolchain mean. Certification first asks lake --version, alone, because lake takes --version only by itself, and refuses a lake that reports another Lean.
• Lean 4.35.0 itself: the generated prelude and goals, and every proof the suite stores, build unchanged with it. verify: Print Lean goals that mean what their obligations mean #54's printer, its unit test (which now runs the pinned Lean too), and verify: Settle what a Lean proof rests on, as a solver's, after certifying it first #55's proofs also pass with it, checked on a local merge of the three.

Tests

• suite/lean_project.cpp:
  • a new project pins v4.35.0;
  • a project pinned to v4.32.2 moves to it with the warning, keeps its proof files, and the next run is quiet;
  • a pin of v4.31.0 is still an error.
• suite/lean_toolchain.test (not on Windows):
  • a fake elan, with lake as its proxy, records what certification asks: +leanprover/lean4:v4.35.0 --version, then +leanprover/lean4:v4.35.0 --dir=… build CppVerify.Generated CppVerify.User;
  • a lake outside elan that reports Lean 4.1.0 is refused with the message above.
  • On main, the log check fails (main runs lake --dir=… build and never names a toolchain), and so does the refusal (main runs the fake lake's build).
• version.test expects the new pin.
• Every test that runs Lean passes on 4.35.0: lean_kernel, lean_certify, lean_fallback, lean_fallback_partial, backend_fidelity_gate, and the rest of the 33.

Mutants of Verifier.cpp, each rebuilt and run against the Lean tests, lean_project.cpp, lean_toolchain.test, and version.test: 7 of 7 killed.

• an earlier pin treated as the user's;
• a moved pin left in the file;
• a pin moved without the warning;
• elan left to run its default;
• lake asked its version together with --dir (lake rejects that, so every certification fails);
• another Lean accepted;
• the version never asked.

Lean differential: every suite file (371 here, the exhaustive uleb128 file aside) exported by main (pin 4.32.2) and by this PR (pin 4.35.0). Each project is built with lake inside it, so that elan runs the toolchain the project pins. The results are identical file by file: 319 build, 28 fail with the same errors (the printer bugs #54 fixes), and 24 produce no project with either binary (tests of rejected input, and the uleb128 variants that need their own flags).

Suites:

• Verify lit, release build: 431 passed, 1 unsupported. VerifyTests, release build: 60 passed, 1 skipped (EncodingParityTest, which needs archives). The assertions build is left to CI.
• The site builds with -W; docs coverage: 0 missing. clang-format: clean.

Rebased onto main after #54 and #55 merged, keeping #54's sentence before the pin in docs/DESIGN.md: the 36 lit tests that run Lean pass.

Docs

• tooling.rst: the pin, how certification runs it, and how a 0.1 project moves to it; the --lean-certify row.
• Book, ch17: the pin and the migration.
• Release notes: "Lean 4.35.0" under running cpp-verify, and the pin under data formats.
• README, ARCHITECTURE.md, DESIGN.md: the pin, and in the architecture the launcher and migration rules.