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.
来源信息
- 仓库
- leanprover/lean4
- 最近来源活动
- 2026年3月1日 07:09
- 检测到的 SKILL.md 语言
- 英语
- 星标
- 9,494
- 分支
- 1,037
安装方式
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
检查来源文件
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
正在显示 SKILL.md
SKILL.md
来源说明 · 只读预览- 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
# 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`.
在 GitHub 查看