mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
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>