7.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 data {
      steps := workload.steps
      samplesPerStep := workload.samplesPerStep
      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.

The application supplies shape and backend labels; the command runner reads arithmetic and device flags through TorchLean's parser. LeanProfiler itself does not inspect tensor values, which keeps its core usable by any Lean application.