Performance guide
Profiling Lean work
A useful profile has a defined scope: one complete command, a repeated benchmark, a ranking of project files, or a trace inside Lean. Measure in that order until the source of the slowdown is clear.
Work from wide measurements to narrow traces
Opening a large trace.profiler tree too early can hide a simpler cause: toolchain synchronization, a lock wait, a cold run compared with a warm one, or one file that became much slower.
One timed run identifies the slow layer. Repeated samples show whether the slowdown is stable. File ranking locates the cost inside the project. A nested Lean trace comes last.
lev --timings build --no-sync --offline
lev profile --warmup 1 --repeat 5
lev inspect performance --files --repeat 3
lev run -- lake env lean -Dtrace.profiler=true Path/SlowFile.leanMeasure one complete run
Before you compare branches or start editing proofs, get one phase split that tells you whether the delay came from lev orchestration, lock waiting, or the delegated command itself.
Collect a small sample set
The report records repeat counts, warmups, raw samples, and summary statistics.
Rank project files
If the command phase still dominates, measure individual modules and identify the slow one.
Trace the selected file
Once the file is clear, the nested Lean trace has a bounded question to answer.
Four questions, four tools
A single wall-clock number is too vague for most Lean performance work. It cannot tell you whether lev prepared an environment, a process waited on a lock, Lake rebuilt a target, or Lean spent the time deep inside one elaboration scope.
lev --timingsOne end-to-end command, split into lev environment, preparation, lock, delegated command, and total phases.lev profileRepeated wall-clock duration of a complete child command, with optional warmups, JSON output, and stable summary fields.lev inspect performance --filesA median-ranked pass over project source files, with saved baselines and regression thresholds.- Lean profilerNested elaborator, metaprogram, kernel, and compiler trace scopes inside one Lean process.
Good questions for the wide tools
- Why did this one build feel slow?
- Did yesterday's import cleanup actually change wall time?
- Is the slowdown in environment work or in the command itself?
Good questions for the narrow tools
- Which file became expensive?
- Which tactic, elaboration pass, or compiler scope dominated inside that file?
- Is the work deterministic enough that heartbeats matter more than wall time?
If --timings says the delegated command dominated, stop investigating locks. If file ranking points to one module, stop treating the whole project as uniformly slow. Each measurement should narrow the next question.
Record enough context to compare runs
Most performance arguments go sideways because people compare unlike runs. A cold build gets compared to a warm one, a new toolchain to an old baseline, or one developer laptop to CI without even naming the difference.
- Name the experiment: cold build, warm no-op build, incremental rebuild after one edit, explicit target, or single-file elaboration.
- Save the JSON report with the summary. It preserves the command, raw samples, run conditions, and schema version.
- Keep the project revision, Lean toolchain, target, machine, and cache policy fixed while comparing runs.
- Stop when the current measurement answers the question. A larger trace is not automatically better evidence.
Related profiling pages
| Page | Contents |
|---|---|
| Timing and samples | Phase timing, warmups, repeated samples, statistics, and JSON reports. |
| Slow files and Lean profiler | Project file ranking, baselines, trace.profiler, Firefox export, and heartbeats. |
| Inspection | Environment drift, dependency selection, and rebuild causes that may resemble performance regressions. |
| Command reference | The profiling and inspection command families in one list. |