LeanProfiler

3.2. Carry repeated context through the loop🔗

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

for (sourcePath, fileIndex) in sourcePaths.zipIdx do
  withStep fileIndex do
    span "source.read" (readSource sourcePath) (metadata := {
      activity := some "filesystem"
    })

    withModule moduleName do
      withPhase "analysis" do
        span "source.analyze" (analyzeSource syntax) (metadata := {
          backend := some analyzerName
        })

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.