// Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance.
Write the Highlights section for Lean 4 release notes. Use when asked to write, draft, or update release highlights for a Lean version.
Extract Zulip thread HTML dumps into readable plain text. Use when the user provides a Zulip HTML file or asks to parse/read/convert/summarize a Zulip thread.
| name | profiling |
| description | Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance. |
| allowed-tools | Bash, Read, Glob, Grep |
Full documentation: script/PROFILER_README.md.
script/lean_profile.sh ./build/release/stage1/bin/lean some_file.lean
Requires samply (cargo install samply) and python3.
samply record --save-only, symbolicate_profile.py, then serve_profile.py.lean_demangle.py works standalone as a stdin filter (like c++filt) for quick name lookups.--raw flag on lean_demangle.py gives exact demangled names without postprocessing (keeps ._redArg, ._lam_0 suffixes as-is).PROFILE_KEEP=1 to keep the temp directory for later inspection.threads[i].stringArray, indexed by threads[i].funcTable.name.