5.2. After main: LeanProfiler🔗

LeanProfiler measures boundaries chosen by the Lean application. A training loop can use names that do not exist inside the compiler or a foreign framework:

profileFromEnvironment "training" do
  for step in List.range steps do
    withStep step do
      span "batch.load" loadBatch
      span "model.forward" forward
      span "loss.backward" backward
      span "optimizer.step" optimizerStep

Its measurements come from Lean and Std runtime APIs:

• IO.monoNanosNow for monotonic span boundaries;

• IO.getTID for the current Lean thread;

• IO.Process.getPID for Trace Event process identity;

• IO.getNumHeartbeats for the current thread's work counter;

• Std.IO.Process.getResourceUsage for session-wide process counters.

Heartbeats add a Lean-specific signal alongside elapsed time. LeanProfiler does not discover operations by itself: the application decides where a span begins, what it is called, and which metadata it carries.

None of these APIs produces accelerator kernel timestamps. A completion hook can synchronize a device and attach allocator counters, but an absent field means “not observed,” not zero.