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,400
- 포크
- 1,019
설치 방법
기본적으로 소스를 먼저 확인하는 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에서 보기