mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
chore: fix profiler shebang and add profiling skill (#12519)
This PR changes the shebang in `lean_profile.sh` from `#!/bin/bash` to `#!/usr/bin/env bash` so the script works on NixOS and other systems where bash is not at `/bin/bash`, and adds a Claude Code skill pointing to the profiler documentation. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
26
.claude/skills/profiling/SKILL.md
Normal file
26
.claude/skills/profiling/SKILL.md
Normal file
@@ -0,0 +1,26 @@
|
||||
---
|
||||
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`.
|
||||
@@ -1,4 +1,4 @@
|
||||
#!/bin/bash
|
||||
#!/usr/bin/env bash
|
||||
# Profile a Lean binary with demangled names.
|
||||
#
|
||||
# Usage:
|
||||
|
||||
Reference in New Issue
Block a user