1. Record your first run🔗

Start with the few boundaries you would name while explaining the program to another person. For a training step, those may be loading, forward evaluation, backward evaluation, and the optimizer. For a server request, they may be parsing, lookup, computation, and serialization. A handful of broad spans is easier to read than hundreds of tiny events, and it usually makes the next question obvious.

Add LeanProfiler to the Lake package that owns the executable:

[[require]]
name = "LeanProfiler"
git = "https://github.com/lean-dojo/LeanProfiler"
rev = "main"

Import the package and put one session around the run. Spans can then name the phases inside it:

import LeanProfiler

open LeanProfiler

def loadBatch : IO Unit :=
  IO.sleep 2

def runForward : IO Unit :=
  IO.sleep 4

def main : IO Unit :=
  profileFromEnvironment "training.step" do
    span "input.load" loadBatch
    span "model.forward" runForward (metadata := {
      phase := some "forward"
      backend := some "eager"
      dtype := some "float32"
      device := some "cpu"
      inputShapes := #["32×784"]
    })

Run the executable with profiling enabled:

LEAN_PROFILE=1 lake exe your_executable

The default files are:

build/leanprofiler-trace.json
build/leanprofiler-summary.json

The trace records every completed span in Trace Event format. Open it in Perfetto to zoom through the run and inspect metadata. The summary groups repeated spans and keeps integer-nanosecond measurements, Lean heartbeats, validation issues, and session resource counters.

Without LEAN_PROFILE=1, profileFromEnvironment still runs the action. It does not retain spans or write reports. Instrumentation can therefore remain in normal application code. Enabled spans still have measurement overhead, so capture only the interval and detail needed for the question.

The session above produces a root event with two children:

training.step
├── input.load
└── model.forward

That small hierarchy already distinguishes a slow loader from a slow model call. Nest narrower spans only after the first trace points to one of them.