This PR replaces three independent name demangling implementations
(Lean, C++, Python) with a single source of truth in
`Lean.Compiler.NameDemangling`. The new module handles the full
pipeline: prefix parsing (`l_`, `lp_`, `_init_`, `initialize_`,
`lean_apply_N`, `_lean_main`), postprocessing (suffix flags, private
name stripping, hygienic suffix stripping, specialization contexts),
backtrace line parsing, and C exports via `@[export]`.
The C++ runtime backtrace handler now calls the Lean-exported functions
instead of its own 792-line reimplementation. This is safe because
`print_backtrace` is only called from `lean_panic_impl` (soft panics),
not `lean_internal_panic`.
The Python profiler demangler (`script/profiler/lean_demangle.py`) is
replaced with a thin subprocess wrapper around a Lean CLI tool,
preserving the `demangle_lean_name` API so downstream scripts work
unchanged.
**New files:**
- `src/Lean/Compiler/NameDemangling.lean` — single source of truth (483
lines)
- `tests/lean/run/demangling.lean` — comprehensive tests (281 lines)
- `script/profiler/lean_demangle_cli.lean` — `c++filt`-style CLI tool
**Deleted files:**
- `src/runtime/demangle.cpp` (792 lines)
- `src/runtime/demangle.h` (26 lines)
- `script/profiler/test_demangle.py` (670 lines)
Net: −1,381 lines of duplicated C++/Python code.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes the compiler removes arguments to join points that are
void, avoiding a bunch of dead
stores in the bytecode and the initial C (though LLVM was surely able to
optimize these away further
down the line already).
This PR replaces the `isImplicitReducible` check with `Meta.isInstance`
in the `shouldInline` function within `inlineCandidate?`.
At the base phase, we skip inlining instances tagged with
`[inline]`/`[always_inline]`/`[inline_if_reduce]` because their local
functions will be lambda lifted during the base phase. The goal is to
keep instance code compact so the lambda lifter can extract
cheap-to-inline declarations. Inlining instances prematurely expands the
code and creates extra work for the lambda lifter — producing many
additional lambda-lifted closures.
The previous check used `isImplicitReducible`, which does not capture
the original intent: some `instanceReducible` declarations are not
instances. `Meta.isInstance` correctly targets only actual type class
instances. Although `Meta.isInstance` depends on the scoped extension
state, this is safe because `shouldInline` runs during LCNF compilation
at `addDecl` time — any instance referenced in the code was resolved
during elaboration when the scope was active, and LCNF compilation
occurs before the scope changes.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ensures the compiler extracts `Array`/`ByteArray`/`FloatArray`
literals as one big closed term to avoid quadratic overhead at closed
term initialization time.
This PR ports the simple ground expression extraction pass from IR to
LCNF.
I locally confirmed that this produces no diff between stage1/stage2 at
the C level (apart from the
changed compiler files) so this should essentially be binary equivalent.
This PR ports the expand reset/reuse pass from IR to LCNF. In addition
it prevents exponential code generation unlike the old one. This results
in a ~15% decrease in binary size and slight speedups across the board.
The change also removes the "is this reset actually used" syntactic
approximation as the previous passes guarantee (at the moment) that all
uses are in the continuation and will thus be caught by this.
This PR enables the module system, in cooperation with the linker, to
separate meta and non-meta code in native binaries. In particular, this
ensures tactics merely used in proofs do not make it into the final
binary. A simple example using `meta import Lean` has its binary size
reduced from 130MB to 1.7MB.
# Breaking change
`importModules (loadExts := true)` must now be preceded by
`enableInitializersExecution`. This was always the case for correct
importing but is now enforced and checked eagerly.
This PR reverts commit 9b7a8eb7c8. After
some more contemplation on
the implications of these changes I think this is not the direction we
want to move into.
This PR avoids false-positive error messages on specialization
restrictions under the module system when the declaration is explicitly
marked as not specializable. It could also provide some minor public
size and rebuild savings.
This PR ports the toposorting pass from IR to LCNF.
We can already do this now as the remaining IR pipeline does not insert
any new auxiliary
declarations into the SCC so now is as good a time as ever to do it.
This PR ensures that failure in initial compilation marks the relevant
definitions as `noncomputable`, inside and outside `noncomputable
section`, so that follow-up errors/noncomputable markings are detected
in initial compilation as well instead of somewhere down the pipeline.
This may require additional `noncomputable` markers on definitions that
depend on definitions inside `noncomputable section` but accidentally
passed the new computability check.
Reported at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Cryptic.20error.20message.20in.20new.20lean.20toolchain.3F.
This PR removes the type correction heuristic from the RC pass as it is
already present in the
boxing pass. Previously the boxing pass did not try to correct types so
the RC pass did. We
discovered issues with not doing this in the boxing pass and
accidentally maintained two corrections
for a while. This PR merges both and removes the one from RC.
This PR makes the derived value analysis in RC insertion recognize
`Array.uget` as another kind of
"projection-like" operation. This allows it to reduce reference count
pressure on elements accessed
through uget.
This PR implements lazy initialization of closed terms. Previous work
has already made sure that ~70% of the closed terms occurring in core
can be statically initialized from the binary. With this the remaining
ones are initialized lazily instead of at startup.
For this we implement a small statically initializable lock that goes
with each term. When trying to access the term we quickly check a flag
to say whether it has already been initialized. If not we take the lock
and initialize it, otherwise we dereference the pointer and fetch the
value.
This PR ports the RC insertion from IR to LCNF.
In doing so it makes the entire code monadic as opposed to simulating a
ReaderT StateRefT stack manually.
This PR renames `instance_reducible` to `implicit_reducible` and adds a
new
`backward.isDefEq.implicitBump` option to prepare for treating all
implicit
arguments uniformly during definitional equality checking.
## Changes
**Rename `instance_reducible` → `implicit_reducible`:**
- Rename `ReducibilityStatus.instanceReducible` constructor to
`implicitReducible`
- Register new `[implicit_reducible]` attribute, keep
`[instance_reducible]` as alias
- Rename `isInstanceReducible` → `isImplicitReducible` (with deprecated
aliases)
- Update all references across src/ and tests/
The rename reflects that this reducibility level is used not just for
instances
but for any definition that needs unfolding during implicit argument
resolution
(e.g., `Nat.add`, `Array.size`).
**Add `backward.isDefEq.implicitBump` option:**
- When `true` (+ `respectTransparency`), bumps transparency to
`.instances` for
ALL implicit arguments in `isDefEqArgs`, not just instance-implicit ones
- Defaults to `false` for staging compatibility — will be flipped to
`true` after
stage0 update
- Adds `// update me!` to `stage0/src/stdlib_flags.h` to trigger CI
stage0 update
## Follow-up (after stage0 update)
- Flip `backward.isDefEq.implicitBump` default to `true`
- Fix resulting test/module failures
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ensures the type resolution cache properly caches results for
type classe containing output parameters.
It ensures the cache key for a query like
```
HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m
```
should be independent of the specific metavariable IDs in output
parameter positions. To achieve this, output parameter arguments are
erased from the cache key. Universe levels that only appear in output
parameter types (e.g., ?u corresponding to the result type's universe)
must also be erased to avoid cache misses when the same query is issued
with different universe metavariable IDs.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR verifies all of the `String` iterators except for the bytes
iterator by relating them to `String.toList`.
Along the way we define `String.posLE` and `String.posLT` analogously to
`String.posGE` and `String.posGT` and redefine `String.prev` to go
through `String.posLT`.
We also define and verify `String.positionsFrom` and
`String.revPositionsFrom`, which are the obvious generaliziations of
`String.positions` and `String.revPositions` starting at a positions
other than the start/end.
Finally, we get various lemmas about strings and positions, including
some nice induction principles `String.Pos.next_induction` and
`String.Pos.prev_induction`.
Of course, we also have all of the analogous results for `String.Slice`.
This is a mitigation for the fact that the upfront noncomputable checker
currently doesn't error out early enough in certain situations so we
violate invariants later on.
This PR adds a simplification rule for `Task.get (Task.pure x) = x` into
the LCNF simplifier. This
ensures that we avoid touching the runtime for a `Task` that instantly
gets destructed anyways.
This PR uses `getImpureSignature?` instead of the `findEnvDecl` from IR
in the LCNF compiler. We
were previously still relying on the IR function because only IR
contained proper borrow
annotations. Now we infer the borrow annotations on the LCNF level and
can thus use the LCNF
signatures.
This PR fixes an issue in LCNF simp where it would attempt to act on
type incorrect `cases`
statements and look for a branch, otherwise panic. This issue did not
yet manifest in production as
various other invariants upheld by LCNF simp help mask it but will start
to become an issue with the
upcoming changes.
This is the proper fix for #6957.
This PR changes the semantics of `inline` annotations in the compiler.
The behavior of the original `@[inline]` attribute remains the same but
the function `inline` now comes with a restriction that it can only use
declarations that are local to the current module. This comes as a
preparation to pulling the compiler out into a separate process.
Closes: #12334
This PR changes the handling of over-applied cases expressions in
`ToLCNF` to avoid generating function declarations that are called
immediately. For example, `ToLCNF` previously produced this:
```lean-4
set_option trace.Compiler.init true
/--
trace: [Compiler.init] size: 4
def test x y : Bool :=
fun _y.1 _y.2 : Bool :=
cases x : Bool
| PUnit.unit =>
fun _f.3 a : Bool :=
return a;
let _x.4 := _f.3 _y.2;
return _x.4;
let _x.5 := _y.1 y;
return _x.5
-/
#guard_msgs in
def test (x : Unit) (y : Bool) : Bool :=
x.casesOn (fun a => a) y
```
which is now simplified to
```lean-4
set_option trace.Compiler.init true
/--
trace: [Compiler.init] size: 3
def test x y : Bool :=
cases x : Bool
| PUnit.unit =>
let a := y;
return a
-/
#guard_msgs in
def test (x : Unit) (y : Bool) : Bool :=
x.casesOn (fun a => a) y
```
This is especially relevant for #8309 because there `dite` is defined as
an over-applied `Bool.casesOn`.
