From 6d305096e5a48af555ffda912f2ccb44ab126706 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sun, 1 Mar 2026 18:09:33 +1100
Subject: [PATCH] chore: fix profiler shebang and add profiling skill (#12519)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 .claude/skills/profiling/SKILL.md | 26 ++++++++++++++++++++++++++
 script/lean_profile.sh            |  2 +-
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 .claude/skills/profiling/SKILL.md

diff --git a/.claude/skills/profiling/SKILL.md b/.claude/skills/profiling/SKILL.md
new file mode 100644
index 0000000000..62e33a0ea8
--- /dev/null
+++ b/.claude/skills/profiling/SKILL.md
@@ -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`.
diff --git a/script/lean_profile.sh b/script/lean_profile.sh
index f2a5501997..5592c9d5c3 100755
--- a/script/lean_profile.sh
+++ b/script/lean_profile.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 # Profile a Lean binary with demangled names.
 #
 # Usage: