This PR adds tooling for profiling Lean programs with human-readable
function names in Firefox Profiler:
- **`script/lean_profile.sh`** — One-command pipeline: record with
samply, symbolicate, demangle, and open in Firefox Profiler
- **`script/profiler/lean_demangle.py`** — Faithful port of
`Name.demangleAux` from `NameMangling.lean`, with a postprocessor that
folds compiler suffixes into compact annotations (`[λ, arity↓]`, `spec
at context[flags]`)
- **`script/profiler/symbolicate_profile.py`** — Resolves raw addresses
via samply's symbolication API
- **`script/profiler/serve_profile.py`** — Serves demangled profiles to
Firefox Profiler without re-symbolication
- **`PROFILER_README.md`** — Documentation including a guide to reading
demangled names
### Example output in Firefox Profiler
| Raw C symbol | Demangled |
|---|---|
| `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` |
| `l_Lean_Meta_foo___redArg___lam__0` | `Lean.Meta.foo [λ, arity↓]` |
| `l_Lean_MVarId_withContext___at__...___spec__2___boxed` |
`Lean.MVarId.withContext [boxed] spec at Lean.Meta.bar[λ, arity↓]` |
Example:
<img width="1145" height="570" alt="image"
src="https://github.com/user-attachments/assets/8d23cc6a-1b89-4c60-9f4a-9f9f0f6e7697"
/>
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
