Logging helpers for training loops

This module defines a small, pluggable logging interface used by the training utilities. The core interface is monad-polymorphic (so it can stay pure), and Logger.stdout provides a convenient IO implementation.

Log levels and entries

inductive Runtime.Autograd.Train.LogLevel : Type

Severity of a log message emitted during training/evaluation.

• debug : LogLevel
• info : LogLevel
• warn : LogLevel
• error : LogLevel

@[implicit_reducible]

instance Runtime.Autograd.Train.instReprLogLevel : Repr LogLevel

def Runtime.Autograd.Train.instReprLogLevel.repr : LogLevel → ℕ → Std.Format

@[implicit_reducible]

instance Runtime.Autograd.Train.instDecidableEqLogLevel : DecidableEq LogLevel

def Runtime.Autograd.Train.LogLevel.render : LogLevel → String

Render a LogLevel as a lower-case string (used by LogEntry.render).

structure Runtime.Autograd.Train.LogEntry : Type

A structured log message (level + string payload).

• level : LogLevel

  Severity level for filtering or rendering.

• message : String

  Human-readable message payload.

def Runtime.Autograd.Train.LogEntry.render (e : LogEntry) : String

Render a LogEntry as [level] msg.

Logger interface

structure Runtime.Autograd.Train.Logger (m : Type → Type) : Type

A small pluggable logger interface used by training utilities.

The interface is compact: a logger consumes a level + string and can live in any monad m (including pure test monads). See Logger.stdout for a basic IO implementation.

• log : LogLevel → String → m Unit

  Emit one message at the requested severity.

def Runtime.Autograd.Train.Logger.noOp {m : Type → Type} [Monad m] : Logger m

A logger that discards every message. Useful as a default.

def Runtime.Autograd.Train.Logger.stdout : Logger IO

A simple IO logger that prints to stdout.

def Runtime.Autograd.Train.Logger.logEntry {m : Type → Type} (logger : Logger m) (entry : LogEntry) : m Unit

Log a pre-built LogEntry.

def Runtime.Autograd.Train.Logger.info {m : Type → Type} (logger : Logger m) (msg : String) : m Unit

Convenience wrapper for an .info message.

def Runtime.Autograd.Train.Logger.warn {m : Type → Type} (logger : Logger m) (msg : String) : m Unit

Convenience wrapper for a .warn message.

def Runtime.Autograd.Train.Logger.error {m : Type → Type} (logger : Logger m) (msg : String) : m Unit

Convenience wrapper for an .error message.

Trainer integration

def Runtime.Autograd.Train.Trainer.withLogger {m : Type → Type} {state a : Type} (t : Trainer m state a) (logger : ℕ → state → StepReport a → m Unit) : Trainer m state a

Attach an arbitrary logger hook to a Trainer (called once per step).

def Runtime.Autograd.Train.Trainer.withReportLogger {m : Type → Type} [Monad m] {state a : Type} [ToString a] (t : Trainer m state a) (logger : Logger m) : Trainer m state a

Attach a Logger to a Trainer by logging the pretty-printed StepReport each step.

This is analogous to printing per-step metrics in an imperative training script (e.g. a PyTorch loop).