LeanProfiler

2.Β Design the captureπŸ”—

The first trace separated input loading from the model's forward pass. That was enough to locate the larger interval, but not enough to compare different steps, modules, devices, or backends. The next capture should add that context without turning every observation into a different event.

Suppose the measured loop looks like this:

let mut parameters := initialParameters
for step in List.range steps do
  let batch ← loadBatch step
  let prediction ← model.forward batch
  let loss := objective prediction batch.targets
  let gradients ← backward loss
  parameters ← optimizer.step parameters gradients

The useful boundaries are already visible in the program: loading, forward evaluation, backward evaluation, and the optimizer update. Start with those four names. A layer name, step number, device, or tensor shape describes the circumstances of one call; it should not replace the name of the work itself.

profileFromEnvironment "training" do
  for step in List.range steps do
    withStep step do
      let batch ← span "batch.load" (loadBatch step)
      let prediction ← span "model.forward" (model.forward batch)
      let loss := objective prediction batch.targets
      let gradients ← span "loss.backward" (backward loss)
      parameters ← span "optimizer.step" (optimizer.step parameters gradients)

This hierarchy remains readable in a ten-step experiment and a ten-thousand-step run. Repeated calls share summary rows, while the trace still preserves every recorded step.

  1. 2.1. Keep names stable and put variation in metadata
  2. 2.2. Carry repeated context through the loop
  3. 2.3. Keep one session around the question
  4. 2.4. Wait for worker tasks that belong to the run
  5. 2.5. Close a span only after asynchronous work finishes
  6. 2.6. Keep long captures finite
  7. 2.7. Give every memory number a precise meaning
  8. 2.8. The resulting event tree