1. Record your first run🔗

Start with the few boundaries you would name while explaining the program to another person. A file indexer may have discovery, parsing, and writing phases. A server request may have parsing, lookup, computation, and serialization. A training step may have loading, forward evaluation, backward evaluation, and an optimizer update. 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 readSource : IO Unit :=
  IO.sleep 2

def analyzeSource : IO Unit :=
  IO.sleep 4

def main : IO Unit :=
  profileFromEnvironment "indexer.run" do
    span "source.read" readSource
    span "source.analyze" analyzeSource (metadata := {
      phase := some "analysis"
      activity := some "source file"
      moduleName := some "indexer"
    })

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:

indexer.run
├── source.read
└── source.analyze

That small hierarchy already distinguishes slow file access from slow analysis. A server, theorem search, simulator, or training loop would use names from its own domain. Nest narrower spans only after the first trace points to one of them.