feat: unify name demangling with single Lean implementation

[kim-em]

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

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 01:23:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-20 06:48:15)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-06 06:53:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a165292462a973c20d3cc8c8b23a3ac2334a2a4a --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-06 10:02:57)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 01:23:10)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-06 06:53:10)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a165292462a973c20d3cc8c8b23a3ac2334a2a4a --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-06 10:02:58)

[hargoniX]

I think the approach in NameDemandling.lean looks generally sensible. It would be great if we could use the new String API to as opposed to the legacy one.

For the linking details in object.cpp I would like to defer to @Kha

[Rob23oba]

Apart from the review comments, I think there should be an option to disable post-processing, since e.g. myFn (λ) can be very ambiguous when a function has many lambdas

[kim-em]

Apart from the review comments, I think there should be an option to disable post-processing, since e.g. myFn (λ) can be very ambiguous when a function has many lambdas

@Rob23oba thanks for your very helpful comments.

Can you point to where you would want to call a version of this with disabled post-processing? I'd like to understand the use case so I can know exactly what should be disabled.

[Rob23oba]

Alright, here's a script that should demonstrate the ambiguity involved:

open Lean Name Demangle
run_meta
  let ext := Compiler.LCNF.impureSigExt
  let env ← getEnv
  let mut map : Std.HashMap String Nat := {}
  for idx in *...env.header.modules.size do
    for decl in ext.getModuleEntries env idx do
      map := map.alter (postprocessNameParts (nameToNameParts decl.name)) fun
        | none => some 1
        | some a => some (a + 1)
  let arr := map.toArray.qsort fun (a, b) (c, d) => b > d ∨ (b = d ∧ a < c)
  let arr := arr.take 100
  Lean.logInfo m!"Result: {arr}"

The top results are

Result: [(Lean.initFn, 276),
 (Lean.initFn [private], 218),
 (Lean.initFn._closed_0, 134),
 (Lean.initFn._closed_1, 126),
 (Lean.initFn._closed_2, 122),
 (Lean.initFn._closed_3, 115),
 (Lean.Server.registerLspRequestHandler spec at Lean.Server.FileWorker.initFn, 111),
 (Lean.initFn [λ], 110),
 (Lean.initFn._closed_4, 109),
 (Lean.initFn._closed_0 [private], 104),
 (Lean.initFn._closed_1 [private], 103),
 (Lean.initFn._closed_2 [private], 102),
 (Lean.initFn._closed_3 [private], 101),
 (Lean.initFn._closed_4 [private], 101),
 (Lean.Meta.initFn, 96),
 (Lean.Meta.initFn [private], 92),
 (Lean.initFn._closed_5 [private], 88),
 (Lean.Compiler.LCNF.initFn [private], 78),
 (Lean.initFn [λ, private], 71),

So if Lean.initFn popped up in the backtrace, there are 276 candidate functions that could have been the cause. This might also be a good test for the postprocessor though because _closed_<n> seems like it should've been converted to [closed] and some of these Lean.initFns have _boxed after the macro scopes. Anyways, even in other cases, it might be good to trace back an error not just to a single function but to a single IR declaration, e.g. when the function is large and you want to narrow down where the error was or when the compiler might have been the problem (i.e. you want to investigate miscompilations).

[kim-em]

Alright, here's a script that should demonstrate the ambiguity involved:

open Lean Name Demangle
run_meta
  let ext := Compiler.LCNF.impureSigExt
  let env ← getEnv
  let mut map : Std.HashMap String Nat := {}
  for idx in *...env.header.modules.size do
    for decl in ext.getModuleEntries env idx do
      map := map.alter (postprocessNameParts (nameToNameParts decl.name)) fun
        | none => some 1
        | some a => some (a + 1)
  let arr := map.toArray.qsort fun (a, b) (c, d) => b > d ∨ (b = d ∧ a < c)
  let arr := arr.take 100
  Lean.logInfo m!"Result: {arr}"

The top results are

Result: [(Lean.initFn, 276),
 (Lean.initFn [private], 218),
 (Lean.initFn._closed_0, 134),
 (Lean.initFn._closed_1, 126),
 (Lean.initFn._closed_2, 122),
 (Lean.initFn._closed_3, 115),
 (Lean.Server.registerLspRequestHandler spec at Lean.Server.FileWorker.initFn, 111),
 (Lean.initFn [λ], 110),
 (Lean.initFn._closed_4, 109),
 (Lean.initFn._closed_0 [private], 104),
 (Lean.initFn._closed_1 [private], 103),
 (Lean.initFn._closed_2 [private], 102),
 (Lean.initFn._closed_3 [private], 101),
 (Lean.initFn._closed_4 [private], 101),
 (Lean.Meta.initFn, 96),
 (Lean.Meta.initFn [private], 92),
 (Lean.initFn._closed_5 [private], 88),
 (Lean.Compiler.LCNF.initFn [private], 78),
 (Lean.initFn [λ, private], 71),

So if Lean.initFn popped up in the backtrace, there are 276 candidate functions that could have been the cause. This might also be a good test for the postprocessor though because _closed_<n> seems like it should've been converted to [closed] and some of these Lean.initFns have _boxed after the macro scopes. Anyways, even in other cases, it might be good to trace back an error not just to a single function but to a single IR declaration, e.g. when the function is large and you want to narrow down where the error was or when the compiler might have been the problem (i.e. you want to investigate miscompilations).

Thanks for the explanation here @Rob23oba.

I think with LEAN_BACKTRACE_RAW available to disable postprocessing in stack traces, I might just proceed for now. But I think this would be good to follow up on, and I'd be happy if you wanted to raise an issue, or suggest a particular place to hook in disabling post-processing.

[hargoniX]

Needs a rebase...