LeanProfiler

2.2. Carry repeated context through the loop🔗

Most labels repeat across several nested spans. Dynamic context records them once:

for step in List.range steps do
  withStep step do
    span "batch.load" (loadBatch step) (metadata := {
      activity := some "data"
    })

    withModule "encoder.block.0" do
      withPhase "forward" do
        span "model.forward" (model.forward batch) (metadata := {
          backend := some backendName
          dtype := some dtypeName
          device := some deviceName
          inputShapes := #[inputShape]
          outputShapes := #[outputShape]
        })

withStep, withModule, and withPhase apply only while their actions run. Nesting them mirrors the lexical structure of the measured program, so a later refactor does not depend on mutable global labels.

An explicit scalar field on a span overrides the surrounding context. Shape arrays inherit from the context only when the span supplies an empty array. This makes a broad module label convenient without preventing one inner operation from naming a more precise module or shape.