Slow files and Lean profiler

Rank files before opening a trace

A native Lean trace is detailed and easy to open too early. If the cause is lock contention, environment synchronization, or one noisy benchmark run, the trace adds reading without addressing the cause. Use it after command-level timing shows that delegated Lean work needs explanation.

Reduce the project to a short list of expensive files, then open the native profiler for the file that remains suspicious.

What Lean's profiler measures

trace.profiler is not a statistical sampler. Lean enters named scopes in its own elaborator, kernel, compiler, and metaprogramming code, accumulates inclusive time for those scopes, then prints or exports the resulting tree. That is why the output uses Lean concepts such as Elab.command, Meta.isDefEq, and Kernel instead of native stack frames.

The trace uses the language of Lean work, which is useful once a file has been isolated. It sees only what Lean instruments; scheduler effects, allocator behavior, and uninstrumented native code still need an external profiler.

Run Lean through lev run -- lake env lean ... here. That keeps the toolchain, dependencies, and environment selection identical to the project run you just measured, instead of quietly profiling a different setup.

Find the slow files before tracing tactics

Most slow projects are not uniformly slow. They have a few ordinary files, a middle band, and one or two expensive files. File mode orders the investigation. Lev discovers project-owned .lean sources, runs one lake build prebuild, then invokes lake lean FILE for each source under the selected environment.

# One measurement per file
lev inspect performance --files

# Three measurements per file, sorted by median duration
lev inspect performance --files --repeat 3

# Record and compare the same experiment
lev inspect performance --files --save-baseline baseline.json
lev inspect performance --files --baseline baseline.json
lev inspect performance --files --baseline baseline.json --max-regression 10

lev: prebuilding project dependencies before file profiling
lev: performance file 1/2: Main.lean
lev: performance file 2/2: Project/Basic.lean
performance: 2 Lean files, 6 measured executions
       7.149 ms  Main.lean
       7.036 ms  Project/Basic.lean

With three repeats per file, lev sorts by median. Trace the files that remain near the top across repeated runs.

The source walk includes symlinked .lean files but does not recurse into symlinked directories. It skips lakefile.lean and generated or dependency trees including .lake, build, lake-packages, target, and node_modules. The prebuild happens once. --warmup N and --repeat N then apply separately to every file. The text table is sorted by median duration, while JSON retains each sample and its summary.

Read the ranking

• Does the same file stay near the top across repeats, or is the ranking mostly noise?
• Is the gap between the slow file and the rest large enough to justify a deeper trace?
• Did only one module regress against the baseline, or did the whole project shift together?

Set a regression threshold

--save-baseline writes the successful run's median for each file together with the exact Lean toolchain. A later run refuses a baseline from another toolchain. With --max-regression 10, any compared file more than 10 percent slower makes the command return status 1.

performance: 2 Lean files, 6 measured executions
       7.366 ms  Project/Basic.lean
       7.177 ms  Main.lean
baseline: 2 compared, 0 new, 0 missing (baseline.json)
slower     +    4.24%       7.067 ->      7.366 ms  Project/Basic.lean
slower     +    2.15%       7.027 ->      7.177 ms  Main.lean

A comparison reports new and missing paths separately. If a file process fails or the run is interrupted, lev keeps the completed per-file records and the child exit code, but omits the aggregate baseline comparison. A partial project should not pass or fail a whole-project regression threshold.

Trace one file with Lean's profiler

When one file or declaration is slow, process timing has done its job. Lean's native profiler can then show nested elaborator and metaprogram work. The most useful modern entry point is trace.profiler.

The raw tree can repeat semantically meaningful elaboration scopes and bury the first useful timing under several parents. People on Lean Zulip keep running into that shape in practice, and Lean issue #5019 asks for broader diagnostics that would surface expensive tactics and typeclass synthesis across a module. lev handles the coarser project-level measurement first, leaving tactic and elaborator diagnosis to Lean's trace.

Learn the trace format on a tiny declaration before opening a real proof. Save this example as ProfilerExample.lean. With the threshold at zero, it exposes elaboration, kernel checking, compiler work, attributes, and linters. Once the nesting makes sense, raise the threshold and move to the slow file.

/-- some doc string -/
@[simp]
def hello := "world"

lev run -- lake env lean \
  -Dtrace.profiler=true \
  -Dtrace.profiler.threshold=0 \
  ProfilerExample.lean

trace.profiler.threshold is a filter: nested scopes below the threshold are omitted from the displayed tree. The default threshold in current Lean releases is 10 milliseconds. Lower it to expose more detail, but expect much larger output and some profiler overhead.

[Elab.command] [0.001532] /-- some doc string -/
    @[simp]
    def hello := "world"
  [Meta.isDefEq] [0.000098] String =?= ?m.2
  [Elab.def.processPreDef] [0.000839] process pre-definitions
    [Kernel] [0.000028] typechecking declarations [hello]
    [compiler] [0.000265] compiling old: [hello]
    [Elab.attribute] [0.000439] applying [simp]

Unrelated instantiation and linter lines are omitted. Command elaboration contains definitional equality and pre-definition processing; pre-definition processing contains kernel, compiler, and attribute work.

Read the first trace

• Read the tallest or widest recurring scopes before the deepest leaf in the tree.
• Ask which parent scope owns the cost. In this tiny example, processPreDef is already the interesting child of Elab.command.
• Only then drill further into kernel, compiler, attributes, typeclass search, or tactic elaboration.

Export a Firefox Profiler trace

For a large trace, use Lean's Firefox Profiler-compatible JSON output instead of reading thousands of terminal lines. Pass the output option when the Lean process starts so the frontend knows to construct the export.

lev run -- lake env lean \
  -Dtrace.profiler=true \
  -Dtrace.profiler.threshold=10 \
  -Dtrace.profiler.output=lean-profile.json \
  MyProject/SlowProof.lean

Open lean-profile.json in Firefox Profiler. The output is structured trace data, not statistical CPU sampling. It visualizes the scopes Lean explicitly instruments, which is much easier to navigate once the terminal tree spills past a few screens.

Wall time, heartbeats, and diagnostics

set_option trace.profiler true
set_option trace.profiler.useHeartbeats true
set_option trace.profiler.threshold 1000

theorem proof_under_test (n : Nat) : n + 0 = n := by
  exact Nat.add_zero n

With trace.profiler.useHeartbeats, trace values are heartbeat counts rather than seconds and the threshold uses heartbeats too. Heartbeats are a deterministic-work budget maintained by Lean. They are useful when elapsed time is noisy or when two machines disagree, but they are not CPU cycles and they do not model I/O or parallel scheduling.

Lean also retains the older profiler option, which reports flatter exclusive timing categories:

lev run -- lake env lean \
  -Dprofiler=true \
  -Dprofiler.threshold=100 \
  MyProject/SlowProof.lean

Use trace.profiler when hierarchy matters. Use the flat profiler for a compact view of exclusive component times. Neither replaces an external sampling profiler when the question is native CPU stacks, allocation, or operating-system behavior.

Limits of Lean's profiler

• lev inspect performance does not attribute time to functions, tactics, or allocations. Command and file modes see only child-process elapsed time.
• --timings does not split Lake's own scheduler or individual module builds.
• Lean trace profiling records instrumented scopes. It is not a sampling profiler and may omit uninstrumented native work.
• Profiling changes execution slightly. Very low trace thresholds can produce enough output to distort the run.
• A warm no-op build says little about a clean build, and a clean build says little about editor feedback after one changed theorem.