6.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.

Lean's profiler option 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 times 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 local timers answer a different question from an application profile. A file can elaborate quickly while its executable spends minutes serving requests or searching a state space.

6.1. Before main: Lean's profilers🔗

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