4.1. Schedule a capture🔗

Long loops rarely need a trace of every step. Startup and compilation can also dominate the first iterations. Schedule.create classifies zero-based steps into skip, warmup, record, and record-and-save phases:

let .ok schedule := Schedule.create
    (skipFirst := 2)
    (wait := 1)
    (warmup := 2)
    (active := 3)
    (repeatCount := 2)
  | throw <| IO.userError "active must be positive"

The example schedule creates two short active captures inside one longer run:

Two repeated capture cycles with skipped, warmup, recorded, and save steps

After the initial skip, each cycle is:

wait → warmup → active

The last active step returns recordAndSave. With active = 1, that only active step records and saves. A zero repeat count continues cycling; a positive repeat count eventually returns skip for every later step.

Schedule.actionAt only classifies. The loop may own capture state itself:

let action := schedule.actionAt step
if action.records then
  recordStep step
else
  runStep step
if action.saves then
  saveCycle

runScheduledCycle runs one complete cycle and opens the session around the active interval:

let ran ← runScheduledCycle schedule cycle config captureName fun step action =>
  runStep step action

Skipped, waiting, and warmup callbacks run before capture begins. They still change model and runtime state, so the active interval begins from the same state the unprofiled training loop would have reached. Give every retained cycle its own trace and summary paths.

The schedule lemmas establish its boundary behavior:

#check LeanProfiler.Schedule.cycleLength_pos
#check LeanProfiler.Schedule.actionAt_eq_skip_of_lt_skipFirst
#check LeanProfiler.ProfilerAction.records_of_saves