5f3ca3ac3d
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>
32 lines
859 B
Text
32 lines
859 B
Text
/-
|
|
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Kim Morrison
|
|
-/
|
|
module
|
|
|
|
import Lean.Compiler.NameDemangling
|
|
|
|
/-!
|
|
Lean name demangler CLI tool. Reads mangled symbol names from stdin (one per
|
|
line) and writes demangled names to stdout. Non-Lean symbols pass through
|
|
unchanged. Like `c++filt` but for Lean names.
|
|
|
|
Usage:
|
|
echo "l_Lean_Meta_foo" | lean --run lean_demangle_cli.lean
|
|
cat symbols.txt | lean --run lean_demangle_cli.lean
|
|
-/
|
|
|
|
open Lean.Name.Demangle
|
|
|
|
def main : IO Unit := do
|
|
let stdin ← IO.getStdin
|
|
let stdout ← IO.getStdout
|
|
repeat do
|
|
let line ← stdin.getLine
|
|
if line.isEmpty then break
|
|
let sym := line.trimRight
|
|
match demangleSymbol sym with
|
|
| some s => stdout.putStrLn s
|
|
| none => stdout.putStrLn sym
|
|
stdout.flush
|