test: add end-to-end test for lake profile

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>

script/PROFILER_README.md

@@ -1,178 +0,0 @@
-# Lean Profiler
-
-Profile Lean programs with demangled names using
-[samply](https://github.com/mstange/samply) and
-[Firefox Profiler](https://profiler.firefox.com).
-
-Python 3, no external dependencies.
-
-## Quick start
-
-```bash
-# One command: record, symbolicate, demangle, and open in Firefox Profiler
-script/lean_profile.sh ./my_lean_binary [args...]
-
-# See all options
-script/lean_profile.sh --help
-```
-
-Requirements: `samply` (`cargo install samply`), `python3`.
-
-## Reading demangled names
-
-The demangler transforms low-level C symbol names into readable Lean names
-and annotates them with compact modifiers.
-
-### Basic names
-
-| Raw symbol | Demangled |
-|---|---|
-| `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` |
-| `lp_std_List_map` | `List.map (std)` |
-| `_init_l_Foo_bar` | `[init] Foo.bar` |
-| `initialize_Init_Data` | `[module_init] Init.Data` |
-| `_lean_main` | `[lean] main` |
-
-### Modifier flags `[...]`
-
-Compiler-generated suffixes are folded into a bracket annotation after the
-name. These indicate *how* the function was derived from the original source
-definition.
-
-| Flag | Meaning | Compiler suffix |
-|---|---|---|
-| `arity`↓ | Reduced-arity specialization | `_redArg` |
-| `boxed` | Boxed calling-convention wrapper | `_boxed` |
-| `impl` | Implementation detail | `_impl` |
-| λ | Lambda-lifted closure | `_lam_N`, `_lambda_N`, `_elam_N` |
-| `jp` | Join point | `_jp_N` |
-| `closed` | Extracted closed subterm | `_closed_N` |
-| `private` | Private (module-scoped) definition | `_private.Module.0.` prefix |
-
-Examples:
-
-```
-Lean.Meta.Simp.simpLambda [boxed, λ]     -- boxed wrapper of a lambda-lifted closure
-Lean.Meta.foo [arity↓, private]           -- reduced-arity version of a private def
-```
-
-Multiple flags are comma-separated. Order reflects how they were collected
-(innermost suffix first).
-
-### Specializations `spec at ...`
-
-When the compiler specializes a function at a particular call site, the
-demangled name shows `spec at <context>` after the base name and its flags.
-The context names the function whose body triggered the specialization, and
-may carry its own modifier flags:
-
-```
-<base-name> [<base-flags>] spec at <context>[<context-flags>]
-```
-
-Examples:
-
-```
--- foo specialized at call site in bar
-Lean.Meta.foo spec at Lean.Meta.bar
-
--- foo (with a lambda closure) specialized at bar (with reduced arity and a lambda)
-Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
-
--- chained specialization: foo specialized at bar, then at baz
-Lean.Meta.foo spec at Lean.Meta.bar spec at Lean.Meta.baz[arity↓]
-```
-
-Context flags use the same symbols as base flags. When a context has no
-flags, the brackets are omitted.
-
-### Other annotations
-
-| Pattern | Meaning |
-|---|---|
-| `<apply/N>` | Lean runtime apply function (N arguments) |
-| `.cold.N` suffix | LLVM cold-path clone (infrequently executed) |
-| `(pkg)` suffix | Function from package `pkg` |
-
-## Tools
-
-### `script/lean_profile.sh` -- Full profiling pipeline
-
-Records a profile, symbolicates it via samply's API, demangles Lean names,
-and opens the result in Firefox Profiler. This is the recommended workflow.
-
-```bash
-script/lean_profile.sh ./build/release/stage1/bin/lean src/Lean/Elab/Term.lean
-```
-
-Environment variables:
-
-| Variable | Default | Description |
-|---|---|---|
-| `SAMPLY_RATE` | 1000 | Sampling rate in Hz |
-| `SAMPLY_PORT` | 3756 | Port for samply symbolication server |
-| `SERVE_PORT` | 3757 | Port for serving the demangled profile |
-| `PROFILE_KEEP` | 0 | Set to 1 to keep the temp directory |
-
-### `script/profiler/lean_demangle.py` -- Name demangler
-
-Demangles individual symbol names. Works as a stdin filter (like `c++filt`)
-or with arguments.
-
-```bash
-echo "l_Lean_Meta_Sym_main" | python3 script/profiler/lean_demangle.py
-# Lean.Meta.Sym.main
-
-python3 script/profiler/lean_demangle.py --raw l_foo___redArg
-# foo._redArg  (exact name, no postprocessing)
-```
-
-As a Python module:
-
-```python
-from lean_demangle import demangle_lean_name, demangle_lean_name_raw
-
-demangle_lean_name("l_foo___redArg")       # "foo [arity↓]"
-demangle_lean_name_raw("l_foo___redArg")   # "foo._redArg"
-```
-
-### `script/profiler/symbolicate_profile.py` -- Profile symbolicator
-
-Calls samply's symbolication API to resolve raw addresses into symbol names,
-then demangles them. Used internally by `lean_profile.sh`.
-
-### `script/profiler/serve_profile.py` -- Profile server
-
-Serves a profile JSON file to Firefox Profiler without re-symbolication
-(which would overwrite demangled names). Used internally by `lean_profile.sh`.
-
-### `script/profiler/lean_demangle_profile.py` -- Standalone profile rewriter
-
-Demangles names in an already-symbolicated profile file (if you have one
-from another source).
-
-```bash
-python3 script/profiler/lean_demangle_profile.py profile.json.gz -o demangled.json.gz
-```
-
-## Tests
-
-```bash
-cd script/profiler && python3 -m unittest test_demangle -v
-```
-
-## How it works
-
-The demangler is a faithful port of Lean 4's `Name.demangleAux` from
-`src/Lean/Compiler/NameMangling.lean`. It reverses the encoding used by
-`Name.mangle` / `Name.mangleAux` which turns hierarchical Lean names into
-valid C identifiers:
-
-- `_` separates name components (`Lean.Meta` -> `Lean_Meta`)
-- `__` encodes a literal underscore in a component name
-- `_xHH`, `_uHHHH`, `_UHHHHHHHH` encode special characters
-- `_N_` encodes numeric name components
-- `_00` is a disambiguation prefix for ambiguous patterns
-
-After demangling, a postprocessing pass folds compiler-generated suffixes
-into human-readable annotations (see [Reading demangled names](#reading-demangled-names)).

script/lean_profile.sh

@@ -1,133 +0,0 @@
-#!/usr/bin/env bash
-# Profile a Lean binary with demangled names.
-#
-# Usage:
-#   script/lean_profile.sh ./my_lean_binary [args...]
-#
-# Records a profile with samply, symbolicates via samply's API,
-# demangles Lean symbol names, and opens the result in Firefox Profiler.
-#
-# Requirements: samply (cargo install samply), python3
-#
-# Options (via environment variables):
-#   SAMPLY_RATE    — sampling rate in Hz (default: 1000)
-#   SAMPLY_PORT    — port for samply symbolication server (default: 3756)
-#   SERVE_PORT     — port for serving the demangled profile (default: 3757)
-#   PROFILE_KEEP   — set to 1 to keep the raw profile after demangling
-
-set -euo pipefail
-
-SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
-PROFILER_DIR="$SCRIPT_DIR/profiler"
-SYMBOLICATE="$PROFILER_DIR/symbolicate_profile.py"
-SERVE_PROFILE="$PROFILER_DIR/serve_profile.py"
-
-usage() {
-    cat >&2 <<EOF
-Usage: $0 [options] <lean-binary> [args...]
-
-Profile a Lean binary and view the results in Firefox Profiler
-with demangled Lean names.
-
-Requirements:
-  samply    cargo install samply
-  python3   (included with macOS / most Linux distros)
-
-Environment variables:
-  SAMPLY_RATE    sampling rate in Hz (default: 1000)
-  SAMPLY_PORT    port for samply symbolication server (default: 3756)
-  SERVE_PORT     port for serving the demangled profile (default: 3757)
-  PROFILE_KEEP   set to 1 to keep the temp directory after profiling
-
-Reading demangled names:
-  Compiler suffixes are shown as modifier flags after the name:
-    [arity↓]   reduced-arity specialization     (_redArg)
-    [boxed]    boxed calling-convention wrapper  (_boxed)
-    [λ]        lambda-lifted closure             (_lam_N, _lambda_N, _elam_N)
-    [jp]       join point                        (_jp_N)
-    [closed]   extracted closed subterm          (_closed_N)
-    [private]  private (module-scoped) def       (_private.Module.0. prefix)
-    [impl]     implementation detail             (_impl)
-
-  Specializations appear after the flags:
-    Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
-      = foo (with lambda closure), specialized at bar (lambda, reduced arity)
-
-  Multiple "spec at" entries indicate chained specializations.
-  See script/PROFILER_README.md for full documentation.
-EOF
-    exit "${1:-0}"
-}
-
-if [ $# -eq 0 ]; then
-    usage 1
-fi
-
-case "${1:-}" in
-    -h|--help) usage 0 ;;
-esac
-
-if ! command -v samply &>/dev/null; then
-    echo "error: samply not found. Install with: cargo install samply" >&2
-    exit 1
-fi
-
-RATE="${SAMPLY_RATE:-1000}"
-PORT="${SAMPLY_PORT:-3756}"
-SERVE="${SERVE_PORT:-3757}"
-TMPDIR=$(mktemp -d /tmp/lean-profile-XXXXXX)
-TMPFILE="$TMPDIR/profile.json.gz"
-DEMANGLED="$TMPDIR/profile-demangled.json.gz"
-SAMPLY_LOG="$TMPDIR/samply.log"
-SAMPLY_PID=""
-
-cleanup() {
-    if [ -n "$SAMPLY_PID" ]; then
-        kill "$SAMPLY_PID" 2>/dev/null || true
-        wait "$SAMPLY_PID" 2>/dev/null || true
-    fi
-    # Safety net: kill anything still on the symbolication port
-    lsof -ti :"$PORT" 2>/dev/null | xargs kill 2>/dev/null || true
-    [ "${PROFILE_KEEP:-0}" = "1" ] || rm -rf "$TMPDIR"
-}
-trap cleanup EXIT
-
-# Step 1: Record
-echo "Recording profile (rate=${RATE} Hz)..." >&2
-samply record --save-only -o "$TMPFILE" -r "$RATE" "$@"
-
-# Step 2: Start samply server for symbolication
-echo "Starting symbolication server..." >&2
-samply load --no-open -P "$PORT" "$TMPFILE" > "$SAMPLY_LOG" 2>&1 &
-SAMPLY_PID=$!
-
-# Wait for server to be ready
-for i in $(seq 1 30); do
-    if grep -q "Local server listening" "$SAMPLY_LOG" 2>/dev/null; then
-        break
-    fi
-    sleep 0.2
-done
-
-# Extract the token from samply's output
-TOKEN=$(grep -oE '[a-z0-9]{30,}' "$SAMPLY_LOG" | head -1)
-
-if [ -z "$TOKEN" ]; then
-    echo "error: could not get samply server token" >&2
-    exit 1
-fi
-
-SERVER_URL="http://127.0.0.1:${PORT}/${TOKEN}"
-
-# Step 3: Symbolicate + demangle
-echo "Symbolicating and demangling..." >&2
-python3 "$SYMBOLICATE" --server "$SERVER_URL" "$TMPFILE" -o "$DEMANGLED"
-
-# Step 4: Kill symbolication server
-kill "$SAMPLY_PID" 2>/dev/null || true
-wait "$SAMPLY_PID" 2>/dev/null || true
-SAMPLY_PID=""
-
-# Step 5: Serve the demangled profile directly (without samply's re-symbolication)
-echo "Opening in Firefox Profiler..." >&2
-python3 "$SERVE_PROFILE" "$DEMANGLED" -P "$SERVE"

script/profiler/lean_demangle.py

@@ -1,82 +0,0 @@
-#!/usr/bin/env python3
-"""
-Lean name demangler — thin wrapper around the Lean CLI tool.
-
-Spawns ``lean --run lean_demangle_cli.lean`` as a persistent subprocess
-and communicates via stdin/stdout pipes. This ensures a single source
-of truth for demangling logic (the Lean implementation in
-``Lean.Compiler.NameDemangling``).
-
-Usage as a filter (like c++filt):
-    echo "l_Lean_Meta_Sym_main" | python lean_demangle.py
-
-Usage as a module:
-    from lean_demangle import demangle_lean_name
-    print(demangle_lean_name("l_Lean_Meta_Sym_main"))
-"""
-
-import atexit
-import os
-import subprocess
-import sys
-
-_process = None
-_script_dir = os.path.dirname(os.path.abspath(__file__))
-_cli_script = os.path.join(_script_dir, "lean_demangle_cli.lean")
-
-
-def _get_process():
-    """Get or create the persistent Lean demangler subprocess."""
-    global _process
-    if _process is not None and _process.poll() is None:
-        return _process
-
-    lean = os.environ.get("LEAN", "lean")
-    _process = subprocess.Popen(
-        [lean, "--run", _cli_script],
-        stdin=subprocess.PIPE,
-        stdout=subprocess.PIPE,
-        stderr=subprocess.DEVNULL,
-        text=True,
-        bufsize=1,  # line buffered
-    )
-    atexit.register(_cleanup)
-    return _process
-
-
-def _cleanup():
-    global _process
-    if _process is not None:
-        try:
-            _process.stdin.close()
-            _process.wait(timeout=5)
-        except Exception:
-            _process.kill()
-        _process = None
-
-
-def demangle_lean_name(mangled):
-    """
-    Demangle a C symbol name produced by the Lean 4 compiler.
-
-    Returns a human-friendly demangled name, or the original string
-    if it is not a Lean symbol.
-    """
-    try:
-        proc = _get_process()
-        proc.stdin.write(mangled + "\n")
-        proc.stdin.flush()
-        result = proc.stdout.readline().rstrip("\n")
-        return result if result else mangled
-    except Exception:
-        return mangled
-
-
-def main():
-    """Filter stdin, demangling Lean names."""
-    for line in sys.stdin:
-        print(demangle_lean_name(line.rstrip("\n")))
-
-
-if __name__ == "__main__":
-    main()

script/profiler/lean_demangle_cli.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-import Lean.Compiler.NameDemangling
-
-/-!
-Lean name demangler CLI tool. Reads mangled symbol names from stdin (one per
-line) and writes demangled names to stdout. Non-Lean symbols pass through
-unchanged. Like `c++filt` but for Lean names.
-
-Usage:
-    echo "l_Lean_Meta_foo" | lean --run lean_demangle_cli.lean
-    cat symbols.txt | lean --run lean_demangle_cli.lean
--/
-
-open Lean.Name.Demangle
-
-def main : IO Unit := do
-  let stdin ← IO.getStdin
-  let stdout ← IO.getStdout
-  repeat do
-    let line ← stdin.getLine
-    if line.isEmpty then break
-    let sym := line.trimRight
-    match demangleSymbol sym with
-    | some s => stdout.putStrLn s
-    | none => stdout.putStrLn sym
-    stdout.flush

script/profiler/lean_demangle_profile.py

@@ -1,117 +0,0 @@
-#!/usr/bin/env python3
-"""
-Lean name demangler for samply / Firefox Profiler profiles.
-
-Reads a profile JSON (plain or gzipped), demangles Lean function names
-in the string table, and writes the result back.
-
-Usage:
-    python lean_demangle_profile.py profile.json -o profile-demangled.json
-    python lean_demangle_profile.py profile.json.gz -o profile-demangled.json.gz
-"""
-
-import argparse
-import gzip
-import json
-import sys
-
-from lean_demangle import demangle_lean_name
-
-
-def _demangle_string_array(string_array):
-    """Demangle Lean names in a string array in-place. Returns count."""
-    count = 0
-    for i, s in enumerate(string_array):
-        if not isinstance(s, str):
-            continue
-        demangled = demangle_lean_name(s)
-        if demangled != s:
-            string_array[i] = demangled
-            count += 1
-    return count
-
-
-def rewrite_profile(profile):
-    """
-    Demangle Lean names in a Firefox Profiler profile dict (in-place).
-
-    Handles two profile formats:
-    - Newer: shared.stringArray (single shared string table)
-    - Older/samply: per-thread stringArray (each thread has its own)
-    """
-    count = 0
-
-    # Shared string table (newer Firefox Profiler format)
-    shared = profile.get("shared")
-    if shared is not None:
-        sa = shared.get("stringArray")
-        if sa is not None:
-            count += _demangle_string_array(sa)
-
-    # Per-thread string tables (samply format)
-    for thread in profile.get("threads", []):
-        sa = thread.get("stringArray")
-        if sa is not None:
-            count += _demangle_string_array(sa)
-
-    return count
-
-
-def process_profile_file(input_path, output_path):
-    """Read a profile, demangle names, write it back."""
-    is_gzip = input_path.endswith('.gz')
-
-    if is_gzip:
-        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
-            profile = json.load(f)
-    else:
-        with open(input_path, 'r', encoding='utf-8') as f:
-            profile = json.load(f)
-
-    count = rewrite_profile(profile)
-
-    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
-
-    if output_path:
-        if out_gzip:
-            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-        else:
-            with open(output_path, 'w', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-    else:
-        json.dump(profile, sys.stdout, ensure_ascii=False)
-        sys.stdout.write('\n')
-
-    return count
-
-
-def main():
-    parser = argparse.ArgumentParser(
-        description="Demangle Lean names in samply/Firefox Profiler profiles")
-    parser.add_argument('input', help='Input profile (JSON or .json.gz)')
-    parser.add_argument('-o', '--output',
-                        help='Output path (default: stdout for JSON, '
-                             'or input with -demangled suffix)')
-    args = parser.parse_args()
-
-    output = args.output
-    if output is None and not sys.stdout.isatty():
-        output = None  # write to stdout
-    elif output is None:
-        # Generate output filename
-        inp = args.input
-        if inp.endswith('.json.gz'):
-            output = inp[:-8] + '-demangled.json.gz'
-        elif inp.endswith('.json'):
-            output = inp[:-5] + '-demangled.json'
-        else:
-            output = inp + '-demangled'
-
-    count = process_profile_file(args.input, output)
-    if output:
-        print(f"Demangled {count} names, wrote {output}", file=sys.stderr)
-
-
-if __name__ == '__main__':
-    main()

script/profiler/serve_profile.py

@@ -1,94 +0,0 @@
-#!/usr/bin/env python3
-"""
-Serve a Firefox Profiler JSON file and open it in the browser.
-
-Unlike `samply load`, this does NOT provide a symbolication API,
-so Firefox Profiler will use the names already in the profile as-is.
-"""
-
-import argparse
-import gzip
-import http.server
-import io
-import sys
-import threading
-import webbrowser
-import urllib.parse
-
-
-class ProfileHandler(http.server.BaseHTTPRequestHandler):
-    """Serve the profile JSON and handle CORS for Firefox Profiler."""
-
-    profile_data = None  # set by main()
-
-    def do_GET(self):
-        if self.path == "/profile.json":
-            self.send_response(200)
-            self.send_header("Content-Type", "application/json")
-            self.send_header("Content-Encoding", "gzip")
-            self.send_header("Access-Control-Allow-Origin", "*")
-            self.end_headers()
-            self.wfile.write(self.profile_data)
-        else:
-            self.send_response(404)
-            self.end_headers()
-
-    def do_OPTIONS(self):
-        # CORS preflight
-        self.send_response(200)
-        self.send_header("Access-Control-Allow-Origin", "*")
-        self.send_header("Access-Control-Allow-Methods", "GET")
-        self.send_header("Access-Control-Allow-Headers", "Content-Type")
-        self.end_headers()
-
-    def log_message(self, format, *args):
-        pass  # suppress request logs
-
-
-def main():
-    parser = argparse.ArgumentParser(
-        description="Serve a profile JSON for Firefox Profiler")
-    parser.add_argument("profile", help="Profile file (.json or .json.gz)")
-    parser.add_argument("-P", "--port", type=int, default=3457,
-                        help="Port to serve on (default: 3457)")
-    parser.add_argument("-n", "--no-open", action="store_true",
-                        help="Do not open the browser")
-    args = parser.parse_args()
-
-    # Read the profile data (keep it gzipped for efficient serving)
-    if args.profile.endswith(".gz"):
-        with open(args.profile, "rb") as f:
-            ProfileHandler.profile_data = f.read()
-    else:
-        with open(args.profile, "rb") as f:
-            raw = f.read()
-        buf = io.BytesIO()
-        with gzip.GzipFile(fileobj=buf, mode="wb") as gz:
-            gz.write(raw)
-        ProfileHandler.profile_data = buf.getvalue()
-
-    http.server.HTTPServer.allow_reuse_address = True
-    server = http.server.HTTPServer(("127.0.0.1", args.port), ProfileHandler)
-    profile_url = f"http://127.0.0.1:{args.port}/profile.json"
-    encoded = urllib.parse.quote(profile_url, safe="")
-    viewer_url = f"https://profiler.firefox.com/from-url/{encoded}"
-
-    if not args.no_open:
-        # Open browser after a short delay to let server start
-        def open_browser():
-            webbrowser.open(viewer_url)
-        threading.Timer(0.5, open_browser).start()
-
-    print(f"Serving profile at {profile_url}", file=sys.stderr)
-    print(f"Firefox Profiler: {viewer_url}", file=sys.stderr)
-    print("Press Ctrl+C to stop.", file=sys.stderr)
-
-    try:
-        server.serve_forever()
-    except KeyboardInterrupt:
-        print("\nStopped.", file=sys.stderr)
-        server.server_close()
-
-
-if __name__ == "__main__":
-    main()

script/profiler/symbolicate_profile.py

@@ -1,198 +0,0 @@
-#!/usr/bin/env python3
-"""
-Symbolicate a raw samply profile using samply's symbolication API,
-then demangle Lean names.
-
-Usage:
-    python symbolicate_profile.py --server http://127.0.0.1:3000/TOKEN \
-        raw-profile.json.gz -o symbolicated-demangled.json.gz
-"""
-
-import argparse
-import gzip
-import json
-import sys
-import urllib.request
-
-from lean_demangle import demangle_lean_name
-
-
-def symbolicate_and_demangle(profile, server_url):
-    """
-    Symbolicate a raw samply profile via the symbolication API,
-    then demangle Lean names. Modifies the profile in-place.
-    Returns the number of names resolved.
-    """
-    libs = profile.get("libs", [])
-    memory_map = [[lib["debugName"], lib["breakpadId"]] for lib in libs]
-
-    count = 0
-    for thread in profile.get("threads", []):
-        count += _process_thread(thread, libs, memory_map, server_url)
-
-    return count
-
-
-def _process_thread(thread, libs, memory_map, server_url):
-    """Symbolicate and demangle one thread. Returns count of resolved names."""
-    sa = thread.get("stringArray")
-    ft = thread.get("frameTable")
-    func_t = thread.get("funcTable")
-    rt = thread.get("resourceTable")
-
-    if not all([sa, ft, func_t, rt]):
-        return 0
-
-    # Build mapping: func_index -> (lib_index, address)
-    # A function may be referenced by multiple frames; pick any address.
-    func_info = {}  # func_idx -> (lib_idx, address)
-    for i in range(ft.get("length", 0)):
-        addr = ft["address"][i]
-        func_idx = ft["func"][i]
-        if func_idx in func_info:
-            continue
-        res_idx = func_t["resource"][func_idx]
-        if res_idx < 0 or res_idx >= rt.get("length", 0):
-            continue
-        lib_idx = rt["lib"][res_idx]
-        if lib_idx < 0 or lib_idx >= len(libs):
-            continue
-        func_info[func_idx] = (lib_idx, addr)
-
-    if not func_info:
-        return 0
-
-    # Batch symbolication: group by lib, send all addresses at once
-    frames_to_symbolicate = []
-    func_order = []  # track which func each frame corresponds to
-    for func_idx, (lib_idx, addr) in func_info.items():
-        frames_to_symbolicate.append([lib_idx, addr])
-        func_order.append(func_idx)
-
-    # Call the symbolication API
-    symbols = _call_symbolication_api(
-        server_url, memory_map, frames_to_symbolicate)
-
-    if not symbols:
-        return 0
-
-    # Update stringArray with demangled names
-    count = 0
-    for func_idx, symbol_name in zip(func_order, symbols):
-        if symbol_name is None:
-            continue
-        demangled = demangle_lean_name(symbol_name)
-        name_idx = func_t["name"][func_idx]
-        if name_idx < len(sa):
-            sa[name_idx] = demangled
-            count += 1
-
-    return count
-
-
-def _call_symbolication_api(server_url, memory_map, frames):
-    """
-    Call the Firefox Profiler symbolication API v5.
-    frames: list of [lib_index, address]
-    Returns: list of symbol names (or None for unresolved frames).
-    """
-    url = server_url.rstrip("/") + "/symbolicate/v5"
-
-    # Send all frames as one "stack" in one job
-    req_body = json.dumps({
-        "memoryMap": memory_map,
-        "stacks": [frames],
-    }).encode()
-
-    req = urllib.request.Request(
-        url,
-        data=req_body,
-        headers={"Content-Type": "application/json"},
-    )
-
-    try:
-        with urllib.request.urlopen(req, timeout=60) as resp:
-            result = json.loads(resp.read())
-    except Exception as e:
-        print(f"Symbolication API error: {e}", file=sys.stderr)
-        return None
-
-    if "error" in result:
-        print(f"Symbolication API error: {result['error']}", file=sys.stderr)
-        return None
-
-    # Extract symbol names from result
-    results = result.get("results", [])
-    if not results:
-        return None
-
-    stacks = results[0].get("stacks", [[]])
-    if not stacks:
-        return None
-
-    symbols = []
-    for frame_result in stacks[0]:
-        if isinstance(frame_result, dict):
-            symbols.append(frame_result.get("function"))
-        elif isinstance(frame_result, str):
-            symbols.append(frame_result)
-        else:
-            symbols.append(None)
-
-    return symbols
-
-
-def process_file(input_path, output_path, server_url):
-    """Read a raw profile, symbolicate + demangle, write it back."""
-    is_gzip = input_path.endswith('.gz')
-
-    if is_gzip:
-        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
-            profile = json.load(f)
-    else:
-        with open(input_path, 'r', encoding='utf-8') as f:
-            profile = json.load(f)
-
-    count = symbolicate_and_demangle(profile, server_url)
-
-    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
-    if output_path:
-        if out_gzip:
-            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-        else:
-            with open(output_path, 'w', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-    else:
-        json.dump(profile, sys.stdout, ensure_ascii=False)
-        sys.stdout.write('\n')
-
-    return count
-
-
-def main():
-    parser = argparse.ArgumentParser(
-        description="Symbolicate a raw samply profile and demangle Lean names")
-    parser.add_argument('input', help='Raw profile (JSON or .json.gz)')
-    parser.add_argument('-o', '--output', help='Output path')
-    parser.add_argument('--server', required=True,
-                        help='Samply server URL (e.g., http://127.0.0.1:3000/TOKEN)')
-    args = parser.parse_args()
-
-    output = args.output
-    if output is None:
-        inp = args.input
-        if inp.endswith('.json.gz'):
-            output = inp[:-8] + '-demangled.json.gz'
-        elif inp.endswith('.json'):
-            output = inp[:-5] + '-demangled.json'
-        else:
-            output = inp + '-demangled'
-
-    count = process_file(args.input, output, args.server)
-    print(f"Symbolicated and demangled {count} names, wrote {output}",
-          file=sys.stderr)
-
-
-if __name__ == '__main__':
-    main()

src/Lean/Compiler/NameDemangling.lean

@@ -13,9 +13,63 @@ import Init.Data.String.Iterate
 import Lean.Data.NameTrie
 public import Lean.Compiler.NameMangling
 
-/-! Human-friendly demangling of Lean compiler symbol names, extending
+/-!
+# Name Demangling
+
+Human-friendly demangling of Lean compiler symbol names, extending
 `Name.demangle` with prefix handling, compiler suffix folding, and backtrace
-line parsing. Called from the C runtime via `@[export]` for backtrace display. -/
+line parsing. Called from the C runtime via `@[export]` for backtrace display.
+
+## Reading demangled names
+
+The demangler transforms low-level C symbol names into readable Lean names
+and annotates them with compact modifiers.
+
+### Basic names
+
+* `l_Lean_Meta_Sym_main` → `Lean.Meta.Sym.main`
+* `lp_std_List_map` → `List.map (std)`
+* `_init_l_Foo_bar` → `[init] Foo.bar`
+* `initialize_Init_Data` → `[module_init] Init.Data`
+* `_lean_main` → `[lean] main`
+
+### Modifier flags
+
+Compiler-generated suffixes are folded into a bracket annotation after the
+name, indicating *how* the function was derived from the source definition:
+
+* `[arity↓]` — reduced-arity specialization (`_redArg`)
+* `[boxed]` — boxed calling-convention wrapper (`_boxed`)
+* `[impl]` — implementation detail (`_impl`)
+* `[λ]` — lambda-lifted closure (`_lam_N`, `_lambda_N`, `_elam_N`)
+* `[jp]` — join point (`_jp_N`)
+* `[closed]` — extracted closed subterm (`_closed_N`)
+* `[private]` — private (module-scoped) definition (`_private.Module.0.` prefix)
+
+Multiple flags are comma-separated: `Lean.Meta.Simp.simpLambda [boxed, λ]`.
+
+### Specializations
+
+When the compiler specializes a function at a call site, the demangled name
+shows `spec at <context>` after the flags. The context may carry its own flags:
+
+* `Lean.Meta.foo spec at Lean.Meta.bar`
+* `Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]`
+
+### Other annotations
+
+* `<apply/N>` — Lean runtime apply function (N arguments)
+* `.cold.N` suffix — LLVM cold-path clone
+* `(pkg)` suffix — function from package `pkg`
+
+## Standalone CLI tool
+
+`script/profiler/lean_demangle_cli.lean` is a `c++filt`-like filter:
+
+```
+echo "l_Lean_Meta_Sym_main" | lean --run script/profiler/lean_demangle_cli.lean
+```
+-/
 
 namespace Lean.Name.Demangle
 

src/lake/Lake/CLI/Help.lean

@@ -23,6 +23,7 @@ COMMANDS:
   build <targets>...    build targets
   query <targets>...    build targets and output results
   exe <exe> <args>...   build an exe and run it in Lake's environment
+  profile <exe>         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
@@ -605,6 +606,28 @@ learn how to specify targets), builds it if it is out of date, and then runs
 it with the given `args` in Lake's environment (see `lake help env` for how
 the environment is set up)."
 
+def helpProfile :=
+"Profile an executable target and demangle Lean names
+
+USAGE:
+  lake profile [OPTIONS] <exe-target> [<args>...]
+
+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/"
+
 def helpLean :=
 "Elaborate a Lean file in the context of the Lake workspace
 
@@ -668,6 +691,7 @@ public def help : (cmd : String) → String
 | "serve"               => helpServe
 | "env"                 => helpEnv
 | "exe" | "exec"        => helpExe
+| "profile"             => helpProfile
 | "lean"                => helpLean
 | "translate-config"    => helpTranslateConfig
 | _                     => usage

src/lake/Lake/CLI/Main.lean

@@ -27,6 +27,7 @@ import Lake.CLI.Build
 import Lake.CLI.Actions
 import Lake.CLI.Translate
 import Lake.CLI.Serve
+import Lake.CLI.Profile
 import Init.Data.String.Modify
 
 -- # CLI
@@ -72,6 +73,10 @@ public structure LakeOptions where
   rev? : Option String := none
   maxRevs : Nat := 100
   shake : Shake.Args := {}
+  profileRate : Nat := 1000
+  profileOutput? : Option String := none
+  profileRaw : Bool := false
+  profileNoServe : Bool := false
 
 def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
   opts.outLv?.getD opts.verbosity.minLogLv
@@ -302,6 +307,15 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--"            => do
   let subArgs ← takeArgs
   modifyThe LakeOptions ({· with subArgs})
+-- Profile options
+| "--rate" => do
+  let r ← takeOptArg "--rate" "sampling rate"
+  modifyThe LakeOptions ({· with profileRate := r.toNat?.getD 1000})
+| "--output" => do
+  let p ← takeOptArg "--output" "output path"
+  modifyThe LakeOptions ({· with profileOutput? := some p})
+| "--raw" => modifyThe LakeOptions ({· with profileRaw := true})
+| "--no-serve" => modifyThe LakeOptions ({· with profileNoServe := true})
 -- Shake options
 | "--keep-implied" => modifyThe LakeOptions ({· with shake.keepImplied := true})
 | "--keep-prefix" => modifyThe LakeOptions ({· with shake.keepPrefix := true})
@@ -921,6 +935,18 @@ protected def exe : CliM PUnit := do
   let exeFile ← ws.runBuild exe.fetch (mkBuildConfig opts)
   exit <| ← (Lake.env exeFile.toString args.toArray).run <| mkLakeContext ws
 
+protected def profile : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let exeSpec ← takeArg "executable target"
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  let exe ← parseExeTargetSpec ws exeSpec
+  let exeFile ← ws.runBuild exe.fetch (mkBuildConfig opts)
+  let _ ← Profile.run exeFile.toString opts.subArgs.toArray opts.profileOutput? opts.profileRate
+    (raw := opts.profileRaw) (serve := !opts.profileNoServe)
+  exit 0
+
 protected def lean : CliM PUnit := do
   processOptions lakeOption
   let leanFile ← takeArg "Lean file"
@@ -1040,6 +1066,7 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "serve"               => lake.serve
 | "env"                 => lake.env
 | "exe" | "exec"        => lake.exe
+| "profile"             => lake.profile
 | "lean"                => lake.lean
 | "translate-config"    => lake.translateConfig
 | "reservoir-config"    => lake.reservoirConfig

src/lake/Lake/CLI/Profile.lean

@@ -0,0 +1,309 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Lean.Data.Json
+import Lean.Compiler.NameDemangling
+public import Lake.Util.Proc
+import Lake.Util.IO
+import Lake.CLI.Error
+import Init.Data.String.Extra
+import Init.Data.String.Search
+import Init.Data.String.TakeDrop
+import Init.System.Uri
+import Init.While
+
+/-!
+# `lake profile`
+
+Profile a Lean executable with [samply](https://github.com/mstange/samply)
+and demangle Lean names for [Firefox Profiler](https://profiler.firefox.com).
+-/
+
+namespace Lake.Profile
+
+open Lean (Json JsonNumber)
+
+/-- Check that a command is available on PATH. -/
+private def requireCmd (cmd : String) (installHint : String) : IO Unit := do
+  let result ← IO.Process.output { cmd := "sh", args := #["-c", s!"command -v {cmd}"] }
+  if result.exitCode != 0 then
+    throw <| IO.userError s!"'{cmd}' not found. {installHint}"
+
+/-- Escape a string for safe interpolation inside a POSIX single-quoted shell argument. -/
+private def shellQuote (s : String) : String :=
+  "'" ++ s.replace "'" "'\\''" ++ "'"
+
+/-- Percent-encode a string for use as a URL path component (RFC 3986).
+    Only unreserved characters (A-Z, a-z, 0-9, `-`, `.`, `_`, `~`) are left unencoded.
+    We can't use `System.Uri.escapeUri` here because it doesn't encode `/`,
+    which must be encoded for the Firefox Profiler `from-url/` route
+    (it splits on `/` to extract the embedded URL as a single path segment). -/
+private def percentEncode (s : String) : String := Id.run do
+  let hexDigit (n : UInt8) : Char :=
+    if n < 10 then Char.ofNat (n.toNat + '0'.toNat)
+    else Char.ofNat (n.toNat - 10 + 'A'.toNat)
+  let mut acc : String := ""
+  for b in s.toUTF8 do
+    if (b >= 0x41 && b <= 0x5A)     -- A-Z
+      || (b >= 0x61 && b <= 0x7A)   -- a-z
+      || (b >= 0x30 && b <= 0x39)   -- 0-9
+      || b == 0x2D || b == 0x2E || b == 0x5F || b == 0x7E  -- - . _ ~
+    then
+      acc := acc.push (Char.ofNat b.toNat)
+    else
+      acc := (acc.push '%').push (hexDigit (b / 16)) |>.push (hexDigit (b % 16))
+  return acc
+
+/-- Extract the samply server token from its log output.
+    Samply prints a URL like `http://127.0.0.1:{port}/{token}/...` (percent-encoded).
+    We decode the URL, split on the known server prefix, and take the first path segment. -/
+private def extractToken (output : String) (port : Nat) : Option String := do
+  let decoded := System.Uri.unescapeUri output
+  let serverUrl := s!"http://127.0.0.1:{port}/"
+  let pos ← decoded.find? serverUrl
+  let suffix ← (decoded.sliceFrom pos).dropPrefix? serverUrl
+  let token := (suffix.takeWhile Char.isAlphanum).toString
+  guard !token.isEmpty
+  return token
+
+/-- Wait for samply server to be ready by polling the stderr log file.
+    Returns the token extracted from the server URL. -/
+private def waitForServer (logFile : String) (proc : IO.Process.Child cfg)
+    (port : Nat) (timeoutMs : Nat := 30000) : IO String := do
+  let startTime ← IO.monoMsNow
+  let mut found := false
+  let mut contents := ""
+  while !found do
+    let now ← IO.monoMsNow
+    if now - startTime > timeoutMs then
+      throw <| IO.userError "timeout waiting for samply server to start"
+    if let some exitCode ← proc.tryWait then
+      contents ← IO.FS.readFile logFile
+      throw <| IO.userError s!"samply exited with code {exitCode}:\n{contents}"
+    IO.sleep 200
+    contents ← IO.FS.readFile logFile
+    if contents.contains "profiler.firefox.com" then
+      found := true
+  match extractToken contents port with
+  | some token => return token
+  | none => throw <| IO.userError "could not extract samply server token"
+
+/-- Build the symbolication request JSON from a raw profile.
+    Returns (request JSON, function map for applying results).
+    The function map entries are (threadIdx, funcIdx, resultFrameIdx). -/
+private def buildSymbolicationRequest (profile : Json)
+    : IO (Json × Array (Nat × Nat × Nat)) := do
+  let libs ← IO.ofExcept <| profile.getObjValAs? (Array Json) "libs"
+  let memoryMap ← libs.mapM fun lib => do
+    let debugName ← IO.ofExcept <| lib.getObjValAs? String "debugName"
+    let breakpadId ← IO.ofExcept <| lib.getObjValAs? String "breakpadId"
+    return Json.arr #[Json.str debugName, Json.str breakpadId]
+  let threads ← IO.ofExcept <| profile.getObjValAs? (Array Json) "threads"
+  let mut frames : Array Json := #[]
+  let mut funcMap : Array (Nat × Nat × Nat) := #[]
+  for hi : threadIdx in [:threads.size] do
+    let thread := threads[threadIdx]
+    let some ft := (thread.getObjValAs? Json "frameTable").toOption | continue
+    let some funcT := (thread.getObjValAs? Json "funcTable").toOption | continue
+    let some rt := (thread.getObjValAs? Json "resourceTable").toOption | continue
+    let some ftFunc := (ft.getObjValAs? (Array Json) "func").toOption | continue
+    let some ftAddr := (ft.getObjValAs? (Array Json) "address").toOption | continue
+    let some ftLen := (ft.getObjValAs? Nat "length").toOption | continue
+    let some funcRes := (funcT.getObjValAs? (Array Json) "resource").toOption | continue
+    let some rtLib := (rt.getObjValAs? (Array Json) "lib").toOption | continue
+    let mut seen : Std.HashSet Nat := {}
+    for i in [:ftLen] do
+      if h1 : i < ftFunc.size then
+        if h2 : i < ftAddr.size then
+          if let some funcIdx := ftFunc[i].getNat?.toOption then
+            if !seen.contains funcIdx then
+              seen := seen.insert funcIdx
+              if hf : funcIdx < funcRes.size then
+                if let some resIdx := funcRes[funcIdx].getNat?.toOption then
+                  if hr : resIdx < rtLib.size then
+                    if let some libIdx := rtLib[resIdx].getNat?.toOption then
+                      frames := frames.push <|
+                        Json.arr #[Json.num (JsonNumber.fromNat libIdx), ftAddr[i]]
+                      funcMap := funcMap.push (threadIdx, funcIdx, frames.size - 1)
+  let req := Json.mkObj [
+    ("memoryMap", Json.arr memoryMap),
+    ("stacks", Json.arr #[Json.arr frames])
+  ]
+  return (req, funcMap)
+
+/-- Parse symbolication response and apply demangled names to the profile. -/
+private def applySymbols (profile : Json) (response : Json)
+    (funcMap : Array (Nat × Nat × Nat)) : IO Json := do
+  let results ← IO.ofExcept <| response.getObjValAs? (Array Json) "results"
+  if h : 0 < results.size then
+    let stacks ← IO.ofExcept <| results[0].getObjValAs? (Array Json) "stacks"
+    if hs : 0 < stacks.size then
+      let frameResults ← IO.ofExcept <| stacks[0].getArr?
+      -- Extract symbol names from response
+      let symbols : Array (Option String) := frameResults.map fun entry =>
+        match entry with
+        | Json.str s => some s
+        | _ => (entry.getObjValAs? String "function").toOption
+      -- Apply demangled names to profile
+      let mut threads ← IO.ofExcept <| profile.getObjValAs? (Array Json) "threads"
+      for (threadIdx, funcIdx, resultIdx) in funcMap do
+        if hr : resultIdx < symbols.size then
+          if let some symbolName := symbols[resultIdx] then
+            let demangled := Lean.Name.Demangle.demangleSymbol symbolName |>.getD symbolName
+            if ht : threadIdx < threads.size then
+              let thread := threads[threadIdx]
+              if let some funcT := (thread.getObjValAs? Json "funcTable").toOption then
+                if let some nameArr := (funcT.getObjValAs? (Array Json) "name").toOption then
+                  if hf : funcIdx < nameArr.size then
+                    if let some nameIdx := nameArr[funcIdx].getNat?.toOption then
+                      if let some sa := (thread.getObjValAs? (Array Json) "stringArray").toOption then
+                        if hn : nameIdx < sa.size then
+                          let sa' := sa.set nameIdx (Json.str demangled)
+                          let thread' := thread.setObjVal! "stringArray" (Json.arr sa')
+                          threads := threads.set threadIdx thread'
+      return profile.setObjVal! "threads" (Json.arr threads)
+  return profile
+
+/-- Kill a child process, ignoring errors (e.g. if it already exited). -/
+private def killSafe {cfg : IO.Process.StdioConfig} (proc : IO.Process.Child cfg) : IO Unit :=
+  try proc.kill; let _ ← proc.wait catch _ => pure ()
+
+/-- Run the full profiling pipeline.
+    Returns the path to the output file. -/
+public def run (binary : String) (args : Array String)
+    (outputPath : Option String := none)
+    (rate : Nat := 1000) (port : Nat := 3756) (raw : Bool := false)
+    (serve : Bool := true) : IO String := do
+  requireCmd "samply" "Install with: cargo install samply"
+  requireCmd "gzip" "gzip is required for profile compression"
+
+  let tmpResult ← IO.Process.output {
+    cmd := "mktemp", args := #["-d", "/tmp/lake-profile-XXXXXX"]
+  }
+  if tmpResult.exitCode != 0 then throw <| IO.userError "failed to create temp directory"
+  let tmpDir := tmpResult.stdout.trimAscii.toString
+  let rawProfile := s!"{tmpDir}/profile.json.gz"
+  let defaultOut := "profile-demangled.json.gz"
+
+  try
+    -- Record
+    IO.eprintln s!"Recording profile (rate={rate} Hz)..."
+    let recordResult ← IO.Process.output {
+      cmd := "samply"
+      args := #["record", "--save-only", "-o", rawProfile,
+                "-r", toString rate, binary] ++ args
+    }
+    if recordResult.exitCode != 0 then
+      IO.eprintln recordResult.stderr
+      throw <| IO.userError s!"samply record failed (exit {recordResult.exitCode})"
+
+    if raw then
+      let out := outputPath.getD "profile-raw.json.gz"
+      let cpResult ← IO.Process.output { cmd := "cp", args := #[rawProfile, out] }
+      if cpResult.exitCode != 0 then
+        throw <| IO.userError s!"failed to copy profile to {out}"
+      IO.eprintln s!"Raw profile: {out}"
+      return out
+
+    -- Start symbolication server
+    -- Use `exec` so killing the shell process also kills samply.
+    IO.eprintln "Starting symbolication server..."
+    let samplyLog := s!"{tmpDir}/samply.log"
+    IO.FS.writeFile samplyLog ""
+    let out := outputPath.getD defaultOut
+    let samplyProc ← IO.Process.spawn {
+      cmd := "sh"
+      args := #["-c",
+        s!"exec samply load --no-open -P {port} {shellQuote rawProfile} \
+          >{shellQuote samplyLog} 2>&1"]
+      stdout := .null
+      stderr := .null
+      stdin := .null
+    }
+    try
+      let token ← waitForServer samplyLog samplyProc port
+      let serverUrl := s!"http://127.0.0.1:{port}/{token}"
+
+      -- Read raw profile by decompressing to temp file
+      IO.eprintln "Symbolicating and demangling..."
+      let rawJson := s!"{tmpDir}/raw.json"
+      let gunzip ← IO.Process.output {
+        cmd := "sh"
+        args := #["-c",
+          s!"zcat {shellQuote rawProfile} > {shellQuote rawJson}"]
+      }
+      if gunzip.exitCode != 0 then
+        throw <| IO.userError "failed to decompress profile"
+      let rawJsonStr ← IO.FS.readFile rawJson
+      let profile ← IO.ofExcept <| Json.parse rawJsonStr
+
+      -- Build and send symbolication request
+      let (symbReq, funcMap) ← buildSymbolicationRequest profile
+      let symbUrl := s!"{serverUrl}/symbolicate/v5"
+      let curl ← IO.Process.output {
+        cmd := "curl"
+        args := #["-sS", "-X", "POST", symbUrl,
+                  "-H", "Content-Type: application/json",
+                  "-d", symbReq.compress]
+      }
+      if curl.exitCode != 0 then
+        throw <| IO.userError s!"symbolication request failed: {curl.stderr}"
+      if curl.stdout.isEmpty then
+        throw <| IO.userError "symbolication returned empty response"
+      let symbResp ← IO.ofExcept <| Json.parse curl.stdout
+
+      -- Apply demangled names and write compressed output
+      let result ← applySymbols profile symbResp funcMap
+      let jsonStr := result.compress
+      let tmpJson := s!"{tmpDir}/demangled.json"
+      IO.FS.writeFile tmpJson jsonStr
+      let gzResult ← IO.Process.output { cmd := "gzip", args := #[tmpJson] }
+      if gzResult.exitCode != 0 then throw <| IO.userError "gzip failed"
+      let mvResult ← IO.Process.output { cmd := "mv", args := #[s!"{tmpJson}.gz", out] }
+      if mvResult.exitCode != 0 then
+        throw <| IO.userError s!"failed to write output to {out}"
+
+      IO.eprintln s!"Demangled {funcMap.size} names, wrote {out}"
+    finally
+      killSafe samplyProc
+
+    unless serve do return out
+
+    -- Serve the demangled profile using samply's HTTP server (which handles CORS,
+    -- works with VSCode port forwarding, etc). We construct the Firefox Profiler URL
+    -- ourselves, omitting `?symbolServer=` so it doesn't re-symbolicate with mangled names.
+    -- TODO: replace samply server with `Std.Http.Server` once #12151 lands.
+    let servePort := port + 1
+    let samplyServeLog := s!"{tmpDir}/samply-serve.log"
+    IO.FS.writeFile samplyServeLog ""
+    let serveProc ← IO.Process.spawn {
+      cmd := "sh"
+      args := #["-c",
+        s!"exec samply load --no-open -P {servePort} {shellQuote out} \
+          >{shellQuote samplyServeLog} 2>&1"]
+      stdout := .null
+      stderr := .null
+      stdin := .null
+    }
+    try
+      let serveToken ← waitForServer samplyServeLog serveProc servePort
+      let profileUrl :=
+        percentEncode s!"http://127.0.0.1:{servePort}/{serveToken}/profile.json"
+      -- Print the server URL so VSCode detects and auto-forwards the port.
+      IO.eprintln s!"Serving on http://127.0.0.1:{servePort}/"
+      IO.eprintln s!"\nOpen in Firefox Profiler:"
+      IO.eprintln s!"  https://profiler.firefox.com/from-url/{profileUrl}"
+      IO.eprintln s!"\nPress Ctrl+C to stop."
+      let _ ← serveProc.wait
+    finally
+      killSafe serveProc
+    return out
+  finally
+    removeDirAllIfExists tmpDir
+
+end Lake.Profile

tests/CMakeLists.txt

@@ -261,6 +261,7 @@ else()
     GLOB_RECURSE LEANLAKETESTS
     "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
     "${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh"
+    "${LEAN_SOURCE_DIR}/../tests/lake/tests/profile/test.sh"
   )
 endif()
 foreach(T ${LEANLAKETESTS})

tests/lake/tests/profile/Main.lean

@@ -0,0 +1,8 @@
+def work : Nat := Id.run do
+  let mut acc := 0
+  for i in [:10000] do
+    acc := acc + i
+  return acc
+
+def main : IO Unit := do
+  IO.println s!"result: {work}"

tests/lake/tests/profile/clean.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+rm -rf .lake lake-manifest.json lake-packages
+rm -f produced.out *.json.gz

tests/lake/tests/profile/lakefile.toml

@@ -0,0 +1,6 @@
+name = "test"
+version = "0.1.0"
+
+[[lean_exe]]
+name = "hello"
+root = "Main"

tests/lake/tests/profile/lean-toolchain

@@ -0,0 +1 @@
+../../../../../build/release/stage1

tests/lake/tests/profile/test.sh

@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Skip if samply is not installed
+if ! command -v samply &>/dev/null; then
+  echo "SKIP: samply not found"
+  exit 0
+fi
+
+# Build the test executable
+test_run build
+
+# Test help output
+test_out "lake profile" help profile
+test_out "--rate" help profile
+test_out "--raw" help profile
+test_out "--no-serve" help profile
+
+# Test --raw mode (records profile, skips symbolication/demangling)
+lake_out profile --raw --output raw.json.gz hello || true
+if match_text "samply record failed" produced.out 2>/dev/null; then
+  echo "SKIP: samply cannot record (missing perf permissions?)"
+  exit 0
+fi
+
+test_exp -f raw.json.gz
+# Verify output is valid gzipped Firefox Profiler JSON
+zcat raw.json.gz | python3 -c "
+import json, sys
+d = json.load(sys.stdin)
+assert 'threads' in d, f'missing threads key, got: {list(d.keys())}'
+assert 'libs' in d, f'missing libs key, got: {list(d.keys())}'
+print(f'raw profile: {len(d[\"threads\"])} threads, {len(d[\"libs\"])} libs')
+"
+
+# Test full pipeline (record + symbolicate + demangle, no serve)
+test_run profile --no-serve --output demangled.json.gz hello
+test_exp -f demangled.json.gz
+
+# Verify demangled output structure
+zcat demangled.json.gz | python3 -c "
+import json, sys
+d = json.load(sys.stdin)
+assert 'threads' in d, f'missing threads key'
+assert 'libs' in d, f'missing libs key'
+# Check that at least some strings exist in the profile
+total_strings = 0
+for t in d['threads']:
+    sa = t.get('stringArray', [])
+    total_strings += len(sa)
+print(f'demangled profile: {len(d[\"threads\"])} threads, {total_strings} strings')
+assert total_strings > 0, 'expected non-empty stringArray in profile threads'
+"
+
+# Cleanup
+rm -f produced.out raw.json.gz demangled.json.gz