Training Reports

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

structure TorchLean.Trainer.Report (α : Type := Float) : Type

Backend-independent training report.

The default trainer API reads binary32 losses back to Float exactly. Typed sessions retain their selected scalar in the structured loss values.

• steps : ℕ

  Number of optimizer updates applied by the session.

• loss : Training.LossProgress α

  Scalar-valued loss measured before and after training.

• arithmetic : Runtime.Arithmetic

  Runtime selector used by open; an explicit scalar in openTyped takes precedence.

• scalarFormat? : Option String

  Exact encoding descriptor when a typed session explicitly selects its scalar.

@[instance_reducible]

instance TorchLean.Trainer.instReprReport {α✝ : Type} [Repr α✝] : Repr (Report α✝)

def TorchLean.Trainer.instReprReport.repr {α✝ : Type} [Repr α✝] : Report α✝ → ℕ → Std.Format

def TorchLean.Trainer.Report.runtimeScalar {α : Type} (report : Report α) : String

Name of the runtime scalar type that produced this report.

def TorchLean.Trainer.Report.summary {α : Type} [ToString α] (report : Report α) : String

One-line summary suitable for quickstarts and scripts.

def TorchLean.Trainer.Report.printSummary {α : Type} [ToString α] (report : Report α) : IO Unit

Print the one-line training summary.

@[instance_reducible]

instance TorchLean.Trainer.Report.instToString {α : Type} [ToString α] : ToString (Report α)