Conversation
The binary is 231 MB, nearly all of it the statically linked Lean library rather than `lean4lean`'s own code. Two changes bring it to 119 MB with no behavioural change. `supportInterpreter` exports every symbol in the executable, which stops `--gc-sections` from dropping anything. The checker replays declarations through the kernel and never interprets Lean source, so it does not need the interpreter. `Lean4Lean/Level.lean` is the only module in the executable's import closure that imports all of `Lean`; it needs only `Lean.Level`. Narrowing it also unblocks a further reduction to roughly 12 MB via `-linitialize_minimal`, once the pinned toolchain is new enough to ship `libinitialize_minimal.a` (leanprover/lean4#14936, first released in v4.35.0). Checked against v4.33.1 by replaying `Init.Data.List.Basic` from oleans (711 declarations) and by parsing a 10 MB export file through `--import`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JPPJuXrRxwXgsWEAqM62dd
Bumps `lean-toolchain` to `nightly-2026-09-06`, with `batteries` on `nightly-testing` and `lean4export` on `master`. `Decidable` is no longer a `class inductive` with `isTrue`/`isFalse` constructors; it is a structure with a `decide : Bool` field and a `reflects_decide : decide.Reflects p` proof, and `Nat.decLe`, `Nat.decEq` and friends now take that shape. Two changes bring `Primitive.lean`'s reflection layer back in line. `Reflection.toDec` builds `⟨b, _⟩` directly, so its `decide` field is literally the reflecting `Bool`. Structure eta and proof irrelevance then match it against the real instances, which the old `dite` form could not: a `dite` on an abstract condition has no `decide` field to project. `Condition.decide` uses the `Decidable.decide` projection instead of `ite _ true false`. Those coincided when `ite` eliminated the `Decidable` inductive directly, but `ite` now goes through `dite`, leaving a `Bool.casesOn` on an abstract `decide` that does not reduce. The reflection proof deliberately uses only `Bool.noConfusion` and `▸`, mirroring `Nat.decLe`'s own proof: the primitive check runs while replaying the primitive itself, so it may only mention constants in that primitive's dependency closure. `Eq.symm` and `Eq.trans` are not. Also drops `reduceNative` and its three call sites. Kernel native reduction is gone, so `Lean.reduceBool` and `Lean.reduceNat` no longer exist; the hook only ever returned `none` or threw on those two constants. Checked by replaying `Init.Data.List.Basic` into a fresh environment (5558 declarations, which exercises every primitive) and through `--import` on a 10 MB export file (4866 declarations), including an export produced by a different Lean build. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JPPJuXrRxwXgsWEAqM62dd
miguelangelorocha
pushed a commit
to iggue/lean4
that referenced
this pull request
Sep 10, 2026
…leanprover#15048) This PR bundles the `lean4lean` external checker with release toolchains, so it can be used as an independent checker without a separate install. Bundles digama0/lean4lean#47, an updated version of the kernel arena branch 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR contains two changes necessary for bundling lean4lean in Lean 4.35 (leanprover/lean4#15048):
Pinned against Lean nightly until rc1 is out.