From a10abb1e002af7e4ff9d395fa92c0cd51d1f1814 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 30 Mar 2026 10:01:01 +0000 Subject: [PATCH 1/3] doc: add `lake profile` command documentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 https://github.com/leanprover/lean4/pull/12545 — do not merge until that PR lands. Co-Authored-By: Claude Opus 4.6 (1M context) --- Manual/BuildTools/Lake/CLI.lean | 40 +++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index df8a26a59f..653e977db4 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -35,6 +35,7 @@ COMMANDS: build ... build targets query ... build targets and output results exe ... build an exe and run it in Lake's environment + profile profile an exe and demangle Lean names check-build check if any default build targets are configured test test the package using the configured test driver check-test check if there is a properly configured test driver @@ -639,6 +640,45 @@ See {lake}`build` for the syntax of target specifications and {lake}`env` for a ::: +```lakeHelp "profile" +Profile an executable target and demangle Lean names + +USAGE: + lake profile [OPTIONS] [...] + +Builds the executable target, records a CPU profile using samply, symbolicates +the raw addresses, demangles Lean compiler names, and writes a Firefox Profiler +JSON file. + +OPTIONS: + --rate N sampling rate in Hz (default: 1000) + --output FILE output path (default: current directory) + --raw skip symbolication and demangling + --no-serve write output file and exit (don't start server) + +REQUIREMENTS: + samply cargo install samply + curl, gzip standard on most systems + +Open the output file in Firefox Profiler at https://profiler.firefox.com/from-file/ +``` + +:::lake profile "«exe-target» [args...]" + +Builds the executable target {lakeMeta}`exe-target`, records a CPU profile using [samply](https://github.com/mstange/samply), symbolicates the raw addresses via samply's API, demangles Lean compiler names, and serves the result for [Firefox Profiler](https://profiler.firefox.com). + +The output is a gzipped Firefox Profiler JSON file with Lean symbol names demangled into human-readable form (e.g. `l_Lean_Meta_foo` becomes `Lean.Meta.foo`). By default, the demangled profile is served on a local HTTP server and a Firefox Profiler URL is printed. + +Options: +* `--rate N` sets the sampling rate in Hz (default: 1000). +* `--output FILE` writes the output to a specific file instead of the current directory. +* `--raw` skips symbolication and demangling, outputting the raw samply profile. +* `--no-serve` writes the output file and exits without starting the server. + +Requires [samply](https://github.com/mstange/samply) (`cargo install samply`). + +::: + ```lakeHelp "clean" Remove build outputs From 6d967e2840318911f416965e5766007d8f65b8b0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 26 Aug 2026 14:46:45 +1000 Subject: [PATCH 2/3] doc: track the rename of `lake profile` to `lake samply` --- Manual/BuildTools/Lake/CLI.lean | 47 ++++++++++++++++++++++++--------- 1 file changed, 34 insertions(+), 13 deletions(-) diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index e1c6a38b75..6d5477248f 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -35,7 +35,7 @@ COMMANDS: build ... build targets query ... build targets and output results exe ... build an exe and run it in Lake's environment - profile profile an exe and demangle Lean names + samply profile an exe with samply and demangle Lean names check-build check if any default build targets are configured test test the package using the configured test driver check-test check if there is a properly configured test driver @@ -644,22 +644,31 @@ See {lake}`build` for the syntax of target specifications and {lake}`env` for a ::: -```lakeHelp "profile" -Profile an executable target and demangle Lean names +```lakeHelp "samply" +Profile an executable target with samply and demangle Lean names USAGE: - lake profile [OPTIONS] [...] + lake samply [OPTIONS] [-- [...] [-- ...]] Builds the executable target, records a CPU profile using samply, symbolicates the raw addresses, demangles Lean compiler names, and writes a Firefox Profiler JSON file. OPTIONS: - --rate N sampling rate in Hz (default: 1000) - --output FILE output path (default: current directory) + -o FILE output path (default: ./profile-demangled.json.gz) --raw skip symbolication and demangling --no-serve write output file and exit (don't start server) +Anything after `--` is forwarded verbatim to `samply record`. An inner `--` +separates samply's own flags from the profiled executable's arguments, e.g.: + + lake samply mergeSort # no samply or exe args + lake samply mergeSort -- --rate 2000 # only samply args + lake samply mergeSort -- -- 10 # only exe args + lake samply mergeSort -- --rate 2000 -- 10 # both + +Run `samply record --help` to see samply's flags. + REQUIREMENTS: samply cargo install samply curl, gzip standard on most systems @@ -667,19 +676,31 @@ REQUIREMENTS: Open the output file in Firefox Profiler at https://profiler.firefox.com/from-file/ ``` -:::lake profile "«exe-target» [args...]" +:::lake samply "[\"-o\" file] [\"--raw\"] [\"--no-serve\"] «exe-target» [\"--\" [«samply-args»...] [\"--\" «exe-args»...]]" -Builds the executable target {lakeMeta}`exe-target`, records a CPU profile using [samply](https://github.com/mstange/samply), symbolicates the raw addresses via samply's API, demangles Lean compiler names, and serves the result for [Firefox Profiler](https://profiler.firefox.com). +Builds the executable target {lakeMeta}`exe-target`, records a CPU profile of it using [samply](https://github.com/mstange/samply), symbolicates the raw addresses, and demangles Lean's compiled names into their source-level form (so `l_Lean_Meta_foo` is reported as `Lean.Meta.foo`). +The result is a gzipped [Firefox Profiler](https://profiler.firefox.com) JSON file. -The output is a gzipped Firefox Profiler JSON file with Lean symbol names demangled into human-readable form (e.g. `l_Lean_Meta_foo` becomes `Lean.Meta.foo`). By default, the demangled profile is served on a local HTTP server and a Firefox Profiler URL is printed. +By default the profile is served on a local HTTP server and a Firefox Profiler URL is printed; `--no-serve` writes the file and exits instead. Options: -* `--rate N` sets the sampling rate in Hz (default: 1000). -* `--output FILE` writes the output to a specific file instead of the current directory. -* `--raw` skips symbolication and demangling, outputting the raw samply profile. +* `-o` writes the profile to {lakeMeta}`file` instead of `./profile-demangled.json.gz`. +* `--raw` skips symbolication and demangling, emitting samply's own profile unchanged. * `--no-serve` writes the output file and exits without starting the server. -Requires [samply](https://github.com/mstange/samply) (`cargo install samply`). +Everything after `--` is forwarded verbatim to `samply record`. +A second `--` separates samply's own flags ({lakeMeta}`samply-args`) from the arguments passed to the profiled executable ({lakeMeta}`exe-args`): + +``` +lake samply mergeSort # no samply or exe args +lake samply mergeSort -- --rate 2000 # only samply args +lake samply mergeSort -- -- 10 # only exe args +lake samply mergeSort -- --rate 2000 -- 10 # both +``` + +Run `samply record --help` for samply's flags. + +Requires [samply](https://github.com/mstange/samply) (`cargo install samply`), along with `curl` and `gzip`. ::: From c3cbf0ed5043d1c4f37b07073fe006668ca80d01 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 10 Sep 2026 16:16:26 +1000 Subject: [PATCH 3/3] doc: track the `lake samply` option changes in leanprover/lean4#12545 --- Manual/BuildTools/Lake/CLI.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index 6d5477248f..06c85d1dd1 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -656,8 +656,8 @@ JSON file. OPTIONS: -o FILE output path (default: ./profile-demangled.json.gz) - --raw skip symbolication and demangling - --no-serve write output file and exit (don't start server) + --raw save the raw profile without serving (default: ./profile-raw.json.gz) + --no-serve write output file and exit without serving it Anything after `--` is forwarded verbatim to `samply record`. An inner `--` separates samply's own flags from the profiled executable's arguments, e.g.: @@ -685,7 +685,7 @@ By default the profile is served on a local HTTP server and a Firefox Profiler U Options: * `-o` writes the profile to {lakeMeta}`file` instead of `./profile-demangled.json.gz`. -* `--raw` skips symbolication and demangling, emitting samply's own profile unchanged. +* `--raw` skips symbolication and demangling, emitting samply's own profile unchanged and without serving it; the default output path becomes `./profile-raw.json.gz`. * `--no-serve` writes the output file and exits without starting the server. Everything after `--` is forwarded verbatim to `samply record`.