3. Read the trace and summary🔗

The nested example recorded seven events on one Lean thread. Its trace preserves the order of the run: each input load is followed by one forward pass, all under one root event. This timeline is generated from the checked-in Trace Event file:

A nested timeline with one root span and alternating input.load and model.forward child spans

The capture came from one real run on Linux with Lean 4.32.0. Its names, nesting, and metadata come from the program. Its durations are observations, not reference performance.

Download the same trace and open it in Perfetto to inspect event arguments and zoom the timeline.

The summary collapses the repeated calls into three rows. The same run printed this table before writing its two files:

Lean profile: 7 events, 1 threads, window 18.44 ms,
recorded thread time 18.44 ms, 290 Lean heartbeats
Process resources: user CPU 0 ms, system CPU 0 ms, peak RSS 59528 KiB, context switches 6

Name                                      Self       Total  Calls      Mean       P95  Self HB      %
model.forward [phase=forward, module=en…  12.17 ms   12.17 ms      3   4.05 ms   4.06 ms        6  66.0%
input.load [phase=input, activity=load]    6.18 ms    6.18 ms      3   2.06 ms   2.06 ms        6  33.5%
example.nested-spans                      89.89 us   18.44 ms      1  18.44 ms  18.44 ms      278   0.4%

Trace: build/leanprofiler-trace.json
Summary: build/leanprofiler-summary.json

The forward calls account for about two thirds of recorded thread time and the loads account for about one third. The enclosing root spans the full run, but almost all of that interval belongs to its children:

Inclusive and self time for the three grouped rows in the nested example

The root is slow because its children are slow, not because of work performed directly in the root. Exact durations move between machines and runs. Event names, grouping fields, call counts, and the relationship between self and total time should remain stable for an unchanged workload.