Training Reports

Small report types returned by the high-level trainer API.

structure TorchLean.Trainer.Report : Type

Backend-independent training report.

Executable scalar backends are read back once at the result boundary, so callers receive ordinary host Float losses without parsing rendered values.

• steps : ℕ

  Number of optimizer steps requested by the configuration.

• loss : Training.LossProgress Float

  Host-readable loss measured before and after training.

• arithmetic : Runtime.Arithmetic

  Arithmetic the run executed under; it fixes the binary32 scalar named by runtimeScalar.

@[instance_reducible]

instance TorchLean.Trainer.instReprReport : Repr Report

def TorchLean.Trainer.instReprReport.repr : Report → ℕ → Std.Format

def TorchLean.Trainer.Report.runtimeScalar (report : Report) : String

Name of the runtime scalar type that produced this report.

def TorchLean.Trainer.Report.summary (report : Report) : String

One-line summary suitable for quickstarts and scripts.

def TorchLean.Trainer.Report.printSummary (report : Report) : IO Unit

Print the one-line training summary.

@[instance_reducible]

instance TorchLean.Trainer.Report.instToString : ToString Report

def TorchLean.Trainer.Report.toTrainLog (title : String) (notes : Array String) (report : Report) : Training.TrainLog

Convert the report into the standard two-point training log.

def TorchLean.Trainer.Report.writeLog (destination : Training.LogDestination) (title : String) (notes : Array String) (report : Report) : IO Unit

Write this report to a log destination when logging is enabled.