feat: add `lake profile` command by kim-em · Pull Request #12545 · leanprover/lean4

kim-em · 2026-02-18T04:29:39Z

This PR adds a lake profile command that records a CPU profile of a Lean executable using
samply, symbolicates addresses, demangles Lean compiler
names, and serves the result to Firefox Profiler.

This replaces the Python scripts in script/profiler/ with a single Lake command.

Depends on feat: unify name demangling with single Lean implementation #12539.

Walkthrough

From the lean4 repo:

$ cd tests/bench/mergeSort
$ lake profile mergeSort -- 10
Building mergeSort
Recording profile (rate=1000 Hz)...
Starting symbolication server...
Symbolicating and demangling...
Demangled 335 names, wrote profile-demangled.json.gz

Serving on http://127.0.0.1:3757/

Open in Firefox Profiler:
  https://profiler.firefox.com/from-url/http%3A%2F%2F127.0.0.1%3A3757%2F...%2Fprofile.json

Press Ctrl+C to stop.

Open the Firefox Profiler URL in your browser. Function names like
List.MergeSort.Internal.mergeSortTR₂ appear instead of their mangled forms.

Options:

--rate N — sampling rate in Hz (default 1000)
--output FILE — save to a specific path
--raw — skip symbolication and demangling
--no-serve — write output file and exit without starting the HTTP server

Test

There's an end-to-end test in tests/lake/tests/profile/ that builds a minimal executable,
runs lake profile --raw and lake profile --no-serve, and validates the output is
well-formed Firefox Profiler JSON. The test gracefully skips when samply isn't installed
or when perf_event_open isn't available.

The test is currently a no-op in CI since samply isn't in the Nix devshell. I'd appreciate
advice on the best way to make it available — adding it to flake.nix buildInputs seemed
heavy (it pulls in the Rust toolchain), but I'm not sure what the preferred approach is.

🤖 Prepared with Claude Code

mathlib-lean-pr-testing · 2026-02-18T06:15:49Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 06:15:49)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c948d24b6ddbb41c199c13edc9ebc04104a667bb --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-07 01:05:08)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c948d24b6ddbb41c199c13edc9ebc04104a667bb --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-30 07:28:34)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-04-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-12 02:23:02)

leanprover-bot · 2026-02-18T06:15:50Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e9cc84b7c99f64220c952dee026ac0f06a031fc4 --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 06:15:50)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c948d24b6ddbb41c199c13edc9ebc04104a667bb --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-07 01:05:10)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c948d24b6ddbb41c199c13edc9ebc04104a667bb --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-30 07:28:36)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-30 11:59:39)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-12 02:23:04)

This PR documents the new `lake profile` command, which builds an executable target, records a CPU profile with samply, symbolicates and demangles Lean compiler names, and serves the result for Firefox Profiler. Depends on leanprover/lean4#12545 — do not merge until that PR lands. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-30T12:55:53Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12545 has successfully built against this PR. (2026-03-30 12:55:51) View Log

This PR adds a `lake profile` command that builds an executable target, records a CPU profile with samply, symbolicates addresses via samply's API, demangles Lean compiler names using `Lean.Name.Demangle.demangleSymbol`, and writes a Firefox Profiler JSON file. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This PR addresses several issues identified during code review: - add try/finally for temp directory cleanup and process lifecycle management - add shellQuote for safe shell argument interpolation - add percentEncode for Firefox Profiler URL construction (can't use escapeUri because it doesn't encode `/`) - check exit codes for cp, mv, gzip, and curl - detect early samply exit in waitForServer via tryWait - rewrite extractToken using modern String APIs (find?, sliceFrom, dropPrefix?, takeWhile) with structural URL prefix matching - remove redundant import of Lean.Compiler.NameDemangling from src/Lean.lean - fix help text: remove broken -o alias, stale PROFILER_README.md reference - use curl -sS for better error diagnostics - fix percentEncode correctness on non-ASCII input (byte-range checks) - reap child processes after kill to avoid zombies Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…shell script This PR updates PROFILER_README.md to reference `lake profile` as the primary profiling workflow, removes references to deleted Python scripts, and deletes `script/lean_profile.sh` which depended on those scripts. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

This PR moves the demangling documentation (modifier flags, specializations, annotations) from the standalone PROFILER_README.md into the module docstring of Lean.Compiler.NameDemangling, where it belongs. The standalone README is deleted since `lake help profile` covers usage and the demangling reference is now with the source. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Add a `--no-serve` flag so the full pipeline (record, symbolicate, demangle) can complete without blocking on the HTTP server. The test builds a minimal executable, runs `lake profile --raw` and `lake profile --no-serve`, and validates the output is well-formed Firefox Profiler JSON. The test gracefully skips when samply is not installed or when perf_event_open is unavailable, so it is currently a no-op in CI. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

On macOS, Apple's `zcat` expects `.Z` files and appends `.Z` to the path, so `zcat profile.json.gz` fails. `gzip -dc` works on both macOS and Linux, and is consistent with the existing `requireCmd "gzip"` check. Also include stderr in the error message for easier debugging. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

hargoniX · 2026-04-13T08:16:48Z

+
+## Standalone CLI tool
+
+`script/profiler/lean_demangle_cli.lean` is a `c++filt`-like filter:


You also delete this file in the PR though?

hargoniX · 2026-04-13T08:18:19Z

+./clean.sh
+
+# Skip if samply is not installed
+if ! command -v samply &>/dev/null; then


This test would never be executed in our current CI environment. I guess we should modify the CI setup to also install samply?

tydeu

The Lake integration looks good to me. Adding this does imply a commitment by us to maintain it in the future, but I presume that has already been agreed on.

tydeu · 2026-04-15T00:40:05Z

+| "--output" => do
+  let p ← takeOptArg "--output" "output path"
+  modifyThe LakeOptions ({· with profileOutput? := some p})


Perhaps -o should also set this option?

tydeu · 2026-04-15T00:42:34Z

+  let _ ← Profile.run exeFile.toString opts.subArgs.toArray opts.profileOutput? opts.profileRate
+    (raw := opts.profileRaw) (serve := !opts.profileNoServe)
+  exit 0


Suggested change

let _ ← Profile.run exeFile.toString opts.subArgs.toArray opts.profileOutput? opts.profileRate

(raw := opts.profileRaw) (serve := !opts.profileNoServe)

exit 0

discard <| Profile.run exeFile.toString opts.subArgs.toArray opts.profileOutput? opts.profileRate

(raw := opts.profileRaw) (serve := !opts.profileNoServe)

The exit should be unnecessary.

tydeu · 2026-04-15T00:49:35Z

@@ -0,0 +1,6 @@
+name = "test"
+version = "0.1.0"


Suggested change

version = "0.1.0"

A version is unnecessary in tests (that do not test versions).

kim-em added the changelog-lake Lake label Feb 18, 2026

kim-em force-pushed the lake-profile branch 4 times, most recently from f9ee312 to bddfb42 Compare February 18, 2026 05:28

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 18, 2026

kim-em force-pushed the lake-profile branch 3 times, most recently from 859a35a to 8510264 Compare February 18, 2026 11:17

kim-em mentioned this pull request Mar 30, 2026

lake: command-specific options should not be accepted globally #13184

Open

kim-em mentioned this pull request Mar 30, 2026

doc: add lake profile command documentation leanprover/reference-manual#817

Open

kim-em force-pushed the lake-profile branch from 5ef61c3 to f2f2143 Compare March 30, 2026 10:59

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 30, 2026

Update lean-toolchain for testing leanprover/lean4#12545

01f57a9

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Mar 30, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 30, 2026

Update lean-toolchain for testing leanprover/lean4#12545

9df350a

mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 30, 2026

kim-em and others added 5 commits April 12, 2026 11:27

kim-em force-pushed the lake-profile branch from f2f2143 to 52ff189 Compare April 12, 2026 01:27

kim-em marked this pull request as ready for review April 12, 2026 03:02

kim-em requested review from hargoniX and leodemoura as code owners April 12, 2026 03:02

kim-em requested a review from tydeu as a code owner April 12, 2026 03:02

hargoniX requested changes Apr 13, 2026

View reviewed changes

tydeu approved these changes Apr 15, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add `lake profile` command#12545

feat: add `lake profile` command#12545
kim-em wants to merge 6 commits intomasterfrom
lake-profile

kim-em commented Feb 18, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Feb 18, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Feb 18, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Mar 30, 2026

Uh oh!

hargoniX Apr 13, 2026

Uh oh!

hargoniX Apr 13, 2026

Uh oh!

tydeu left a comment

Uh oh!

tydeu Apr 15, 2026

Uh oh!

tydeu Apr 15, 2026

Uh oh!

tydeu Apr 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants


		## Standalone CLI tool

		`script/profiler/lean_demangle_cli.lean` is a `c++filt`-like filter:

Conversation

kim-em commented Feb 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Walkthrough

Test

Uh oh!

mathlib-lean-pr-testing bot commented Feb 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Feb 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Mar 30, 2026

Uh oh!

hargoniX Apr 13, 2026

Choose a reason for hiding this comment

Uh oh!

hargoniX Apr 13, 2026

Choose a reason for hiding this comment

Uh oh!

tydeu left a comment

Choose a reason for hiding this comment

Uh oh!

tydeu Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

tydeu Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

tydeu Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

kim-em commented Feb 18, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Feb 18, 2026 •

edited

Loading

leanprover-bot commented Feb 18, 2026 •

edited

Loading