feat: remove deprecated in-kernel native reduction - #14953
Merged
Conversation
This PR removes `Lean.reduceBool`, `Lean.reduceNat`, `Lean.ofReduceBool`, `Lean.ofReduceNat` and `Lean.trustCompiler`, along with the kernel's support for reducing applications of the first two by running the compiler. They have been deprecated since 2026-02-01 in favour of asserting native evaluations with axioms, which is what `native_decide` and `bv_decide` already do through `Lean.Meta.nativeEqTrue`. Nothing in the toolchain used them any more. `Lean.Meta.reduceNative?`, `Lean.Meta.reduceBoolNative`, `Lean.Meta.reduceNatNative` and `Lean.Meta.isDefEqNative` go with them, since they exist only to reduce those two constants. Downstream callers of `reduceNative?` should drop the call: with the constants gone it could only ever return `none`. `test_extern` wrapped its comparison in `Lean.reduceBool` before handing it to `evalExpr`, where the wrapper was the identity; it now evaluates the decision directly. Removing the axioms also makes `#print axioms` mean what it says for the whole environment. `Lean.trustCompiler` was referenced unconditionally from the bodies of `reduceBool` and `reduceNat` so that it would be reported for anything reducing through them, which left it looking used in every environment that merely imported them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This PR removes `run_boxed_kernel` and `elab_environment_of_kernel_env`, which existed only so the kernel could run a compiled declaration while reducing `Lean.reduceBool` and `Lean.reduceNat`. With in-kernel native reduction gone, they have no callers, and `src/kernel/` no longer refers to the interpreter or to `ir` at all. `Environment.ofKernelEnv` loses its `@[export]` with them; the function itself stays, since `Lean.Message` and `Lean.Replay` use it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
breaks-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
nomeata
approved these changes
Aug 28, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 28, 2026
|
The adaptation PR for this PR is leanprover/downstream-lean4#27. |
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Aug 28, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Aug 28, 2026
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
3 participants
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 removes
Lean.reduceBool,Lean.reduceNat,Lean.ofReduceBool,Lean.ofReduceNatandLean.trustCompiler, along with the kernel's support for reducing applications of the first two by running the compiler. They have been deprecated since 2026-02-01 in favour of asserting native evaluations with axioms, which is whatnative_decideandbv_decidealready do throughLean.Meta.nativeEqTrue. Nothing in the toolchain used them any more.Removing the axioms makes
#print axioms, and the upcominglake check, mean what it says for the whole environment.Lean.trustCompilerwas referenced unconditionally from the bodies ofreduceBoolandreduceNatso that it would be reported for anything reducing through them, which left it looking used in every environment that merely imported them.