6.4. Instrument a TorchLean trainer🔗

The MLP executable profiles the real Trainer.train call and then measures a distribution of predictions. Its central block is:

profile config "torchlean.mlp-training" do
  let trained ← span "model.train"
    (trainer.train buildDataset {
      steps := workload.steps
      batchSize := workload.batchSize
      logEvery := 0
    })
    (metadata := {
      modelMetadata with
      phase := some "training"
      activity := some "training run"
    })

  for iteration in List.range workload.predictionRuns do
    withStep iteration do
      span "model.predict" (trained.predict heldout) (metadata := {
        modelMetadata with
        phase := some "inference"
        activity := some "held-out prediction"
      })

model.train measures the whole trainer call. It cannot split batches, forward evaluation, backward evaluation, and optimizer updates from outside that call. If the trace points into training, place narrower spans in the training loop that owns those phases. Prediction is different: the caller owns every repeated call, so each one can carry a step index while all calls share one summary row.

Shape, dtype, backend, and device labels come from the TorchLean integration. LeanProfiler itself does not inspect tensor values, which keeps its core usable by any Lean application.