2.2. Reservation establishes the event tree
Before the timed action starts, LeanProfiler reserves an event index under a mutex. The reservation reads the current Lean thread identifier and the innermost active span on that thread. It records:
Field | Meaning at reservation time |
|---|---|
| a monotonically increasing event identifier |
| the active local parent, or an explicitly supplied cross-thread parent |
| the event's nesting depth in the logical tree |
| the Lean execution thread that admitted the span |
inherited metadata | dynamic phase, module, step, and related context |
The index is reserved before the action because completion order is not execution order. A short child may finish before its parent, and two worker threads may finish in either order. Export sorts events by their reservation indices, while every event also keeps its actual start and stop times.
Each Lean thread has its own nesting stack. This prevents concurrent work from becoming accidental siblings or children merely because another thread happened to open a span first. When a caller spawns a worker, it can explicitly pass the current parent index to that worker; the trace then keeps the causal link without pretending that the two threads share one clock.