# Profiling

> Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance.

- Skill: `leanprover/profiling` (Agent Skill)
- Install (CLI): `npx skillmds@latest add leanprover/profiling`
- Raw SKILL.md: https://api.skillmd.com/api/skills/leanprover/profiling/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: leanprover (https://skillmd.com/u/leanprover)
- Updated: 2026-09-10
- Page: https://skillmd.com/skills/leanprover/profiling

---


# Profiling Lean Programs

Full documentation: `script/PROFILER_README.md`.

## Quick Start

```bash
script/lean_profile.sh ./build/release/stage1/bin/lean some_file.lean
```

Requires `samply` (`cargo install samply`) and `python3`.

## Agent Notes

- The pipeline is interactive (serves to browser at the end). When running non-interactively, run the steps manually instead of using the wrapper script.
- The three steps are: `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.
- The `--raw` flag on `lean_demangle.py` gives exact demangled names without postprocessing (keeps `._redArg`, `._lam_0` suffixes as-is).
- Use `PROFILE_KEEP=1` to keep the temp directory for later inspection.
- The demangled profile is a standard Firefox Profiler JSON. Function names live in `threads[i].stringArray`, indexed by `threads[i].funcTable.name`.