5.1. Before `main`: Lean's profilers🔗

Use Lean's command-line profile when a declaration makes a file slow to build:

lake env lean --profile MyProject/SlowModule.lean

It reports elaboration and type-checking time by declaration. Use it when an import or theorem became expensive before the executable starts.

The component profiler accumulates exclusive time inside instrumented elaborator and compiler components:

lake env lean \
  -Dprofiler=true \
  -Dprofiler.threshold=10 \
  MyProject/SlowModule.lean

The threshold is in milliseconds. The default is 100 milliseconds.

trace.profiler keeps Lean's nested trace tree and can export a Firefox-Profiler-compatible file:

lake env lean \
  -Dtrace.profiler=true \
  -Dtrace.profiler.threshold=5 \
  -Dtrace.profiler.output=build/elaboration-profile.json \
  MyProject/SlowModule.lean

With -Dtrace.profiler.useHeartbeats=true, its measurement and threshold use heartbeats. trace.profiler.serve starts an ephemeral loopback server and opens Firefox Profiler. The server shuts down after the profile is fetched.

Two smaller tools answer local questions:

IO.timeit prints elapsed time for one IO action;
IO.allocprof invokes Lean's runtime allocation-profiler hook.

These tools do not replace an application runtime profile. A file can elaborate quickly while its executable spends minutes in a training loop.

5.1. Before main: Lean's profilers🔗

5.1. Before `main`: Lean's profilers🔗