Skip to content

Commit 55c8ccb

Browse files
kim-emclaude
andcommitted
feat: unify name demangling with single Lean implementation
This PR replaces three independent name demangling implementations (Lean, C++, Python) with a single source of truth in Lean. The new `Lean.Compiler.NameDemangling` module handles the full pipeline: prefix parsing, postprocessing (suffix flags, private names, hygienic stripping, specialization contexts), backtrace line parsing, and C exports. The C++ runtime backtrace handler now calls `@[export]`ed Lean functions instead of its own reimplementation. The Python profiler demangler is replaced with a thin subprocess wrapper around a Lean CLI tool. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent e9cc84b commit 55c8ccb

File tree

10 files changed

+864
-2245
lines changed

10 files changed

+864
-2245
lines changed

script/profiler/lean_demangle.py

Lines changed: 52 additions & 749 deletions
Large diffs are not rendered by default.
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
/-
2+
Copyright (c) 2025 Microsoft Corporation. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kim Morrison
5+
-/
6+
module
7+
8+
import Lean.Compiler.NameDemangling
9+
10+
/-!
11+
Lean name demangler CLI tool. Reads mangled symbol names from stdin (one per
12+
line) and writes demangled names to stdout. Non-Lean symbols pass through
13+
unchanged. Like `c++filt` but for Lean names.
14+
15+
Usage:
16+
echo "l_Lean_Meta_foo" | lean --run lean_demangle_cli.lean
17+
cat symbols.txt | lean --run lean_demangle_cli.lean
18+
-/
19+
20+
open Lean.Name.Demangle
21+
22+
def main : IO Unit := do
23+
let stdin ← IO.getStdin
24+
let stdout ← IO.getStdout
25+
repeat do
26+
let line ← stdin.getLine
27+
if line.isEmpty then break
28+
let sym := line.trimRight
29+
match demangleSymbol sym with
30+
| some s => stdout.putStrLn s
31+
| none => stdout.putStrLn sym
32+
stdout.flush

0 commit comments

Comments
 (0)