2.3. Keep one session around the question🔗

One profile call owns one capture buffer and produces one trace-summary pair. At the beginning of the session it clears old events and enables recording. At the end it disables recording, checks the event structure, computes summary rows, and writes both artifacts.

def profileTraining (config : ProfilerConfig) : IO Unit :=
  profile config "training" do
    runTrainingLoop

Nested span calls are normal. Nested or overlapping profile calls are rejected because two sessions cannot safely own the same process-wide buffer or output paths.

The session also preserves the failure that matters. If runTrainingLoop throws, LeanProfiler first attempts to export the completed spans and then rethrows the original exception. If export fails as well, the export error is printed, but it does not hide the training failure. A partial trace from a failed run is useful diagnostic evidence; it is not automatically a valid benchmark.