Conversation
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>
…n link dependency The `@[export lean_demangle_bt_line_cstr]` function is defined in `Lean.Compiler.NameDemangling` (in `libLean`) but called from `libleanrt` (`print_backtrace`). On Linux these are in separate linker groups, so downstream executables fail to link with undefined reference. Use a weak symbol with a no-op stub so `leanrt` doesn't require `libLean` at link time. When the Lean demangler is linked in (as it always is for Lean executables), the real implementation overrides the stub. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
kim-em
force-pushed
the
lake-profile
branch
4 times, most recently
from
f9ee312 to
bddfb42
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
kim-em
force-pushed
the
lake-profile
branch
2 times, most recently
from
1e615a4 to
859a35a
Compare
This PR adds a `lake profile` command that builds an executable target, records a CPU profile with samply, symbolicates addresses via samply's API, demangles Lean compiler names using `Lean.Name.Demangle.demangleSymbol`, and writes a Firefox Profiler JSON file. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
# Conflicts: # script/profiler/lean_demangle.py # src/Lean/Compiler/NameDemangling.lean # src/runtime/object.cpp # tests/elab/demangling.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a
lake profilecommand that records a CPU profile of a Lean executable usingsamply, symbolicates addresses, demangles Lean compiler
names, and serves the result to Firefox Profiler.
This replaces the Python scripts in
script/profiler/with a single Lake command.Depends on #12539.
Walkthrough
From the lean4 repo:
Open the Firefox Profiler URL in your browser. Function names like
List.MergeSort.Internal.mergeSortTR₂appear instead of their mangled forms.Options:
--rate N— sampling rate in Hz (default 1000)--output FILE— save to a specific path--raw— skip symbolication and demangling🤖 Prepared with Claude Code