Training Reports

Training curves, metric histories, and logs produced by Trainer runs.

def TorchLean.Training.shouldReport (every completed : ℕ) : Bool

Return whether a completed step should emit a periodic report.

def TorchLean.Training.writeLog (path : System.FilePath) (log : TrainLog) : IO Unit

Write a training log as JSON and report the output path.

def TorchLean.Training.writeLogTo (destination : LogDestination) (log : TrainLog) : IO Unit

Write a training log to an enabled or disabled destination.

def TorchLean.Training.writeLossComparison (path : System.FilePath) (title : String) (steps : ℕ) (beforeLoss afterLoss : Float) (notes : Array String := #[]) : IO Unit

Write a log containing the loss before and after a fixed number of training steps.

def TorchLean.Training.writeLossComparisonTo (destination : LogDestination) (title : String) (steps : ℕ) (beforeLoss afterLoss : Float) (notes : Array String := #[]) : IO Unit

Write a before-and-after loss log to an enabled or disabled destination.

structure TorchLean.Training.CurveEndpoints : Type

First and last values of a nonempty scalar training curve.

• finalStep : ℕ

  Step associated with the final value.

• first : Float

  First recorded value.

• last : Float

  Last recorded value.

def TorchLean.Training.instReprCurveEndpoints.repr : CurveEndpoints → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Training.instReprCurveEndpoints : Repr CurveEndpoints

def TorchLean.Training.Curve.endpoints? (curve : Curve) : Option CurveEndpoints

Return the endpoints of a scalar curve, or none when it contains no values.

def TorchLean.Training.Curve.endpoints (curve : Curve) (context : String := "training curve") : IO CurveEndpoints

Return the endpoints of a scalar curve or raise a contextual error when it is empty.

def TorchLean.Training.Curve.printLossSummary (curve : Curve) (steps : ℕ) : IO Unit

Print the first and last loss from a scalar training curve.

def TorchLean.Training.Curve.writeLog (curve : Curve) (path : System.FilePath) (title : String) (seriesName : String := "loss") (notes : Array String := #[]) : IO Unit

Write a scalar curve as a one-series training log.

def TorchLean.Training.Curve.writeLogTo (curve : Curve) (destination : LogDestination) (title : String) (seriesName : String := "loss") (notes : Array String := #[]) : IO Unit

Write a scalar curve to an enabled or disabled training-log destination.