Training Logs

Pure training-log data plus the stable JSON codec used by examples, widgets, and CLI artifacts.

The data structures in this file are compact:

• Series is one named scalar metric, such as loss or accuracy;
• Curve is the convenient builder for one metric over time;
• MetricHistory is the convenient builder for several aligned metrics; and
• TrainLog is the persisted/viewed artifact shared by JSON IO and widgets.

For W&B-style workflows, ExperimentLog adds run metadata, config entries, tags, and artifact references while still lowering to the same stable TrainLog JSON that TorchLean widgets already know how to render. This gives examples one clean local artifact format and a straightforward bridge to hosted trackers.

Metric values are Float on purpose. A logged loss or accuracy is a reporting scalar that has already left the generic α optimizer layer: it is converted once at the call site and then only compared, plotted, and written as a JSON number. Generalising the log over α would push a ToJson/FromJson obligation onto every scalar type for no gain in precision.

We keep JSON support in the same module as the data model so there is one canonical logging API: Runtime.Training.TrainLog.writeJson / readJson. Widgets live in NN.Widgets.Runtime.Training and render these logs in the infoview.

Core Artifact Model

TorchLean logs are local artifacts with a schema that mirrors the useful scalar-metric subset of hosted experiment trackers such as Weights & Biases:

• a run has project/name/id metadata,
• config records hyperparameters and data choices,
• metric history records scalar values over steps,
• artifacts point to files produced by the run.

The data stays simple and serializes to ordinary JSON, so examples can write it without any network service or background process.

structure Runtime.Training.ConfigEntry : Type

A string-valued hyperparameter/config entry attached to a run.

• key : String

  Config key, for example "lr", "optimizer", or "dataset".

• value : String

  Display value. Keep this stringly-typed so JSON artifacts stay tool-agnostic.

@[instance_reducible]

instance Runtime.Training.instInhabitedConfigEntry : Inhabited ConfigEntry

structure Runtime.Training.Artifact : Type

A file artifact produced or consumed by a training run.

• name : String

  Short artifact name, for example "checkpoint" or "predictions_csv".

• path : System.FilePath

  Local path to the artifact. External trackers may use this path when uploading artifacts.

• kind : String

  Optional kind, such as "model", "plot", "dataset", or "report".

• description : String

  Optional description shown beside the metric.

@[instance_reducible]

instance Runtime.Training.instInhabitedArtifact : Inhabited Artifact

structure Runtime.Training.RunInfo : Type

Run metadata for a local experiment.

The fields line up with the common tracker vocabulary (project, name, group, tags, config), but the value is plain Lean data and performs no network IO.

• project : String

  Project or collection name. Examples usually use "torchlean".

• name : String

  Display name for this run. Defaults to the resulting TrainLog.title if left empty.

• runId : String

  Stable run identifier, useful when several artifacts belong to one run.

• group : String

  Optional group/sweep name.

• tags : Array String

  Tags for filtering/comparing runs.

• config : Array ConfigEntry

  String-valued hyperparameters and data/runtime choices.

@[instance_reducible]

instance Runtime.Training.instInhabitedRunInfo : Inhabited RunInfo

structure Runtime.Training.Series : Type

A named scalar metric series over training steps (e.g. loss/accuracy/LR).

• name : String

  Display name (e.g. "loss" or "val_acc").

• values : Array Float

  Scalar values over steps.

• color : String

  CSS color hint used by viewers.

@[instance_reducible]

instance Runtime.Training.instInhabitedSeries : Inhabited Series

structure Runtime.Training.TrainLog : Type

A small multi-series training log (curves + optional notes).

• title : String

  Title shown at the top of viewers.

• steps : Array Nat

  Optional step indices.

  If empty, viewers typically use 0..(n-1).

• series : Array Series

  One or more metric series (should have compatible lengths).

• notes : Array String

  Free-form notes (hyperparameters, dataset, run id, etc.).

def Runtime.Training.TrainLog.lossComparison (title : String) (steps : Nat) (lossBefore lossAfter : Float) (notes : Array String := #[]) (color : String := "#4e79a7") : TrainLog

Build a two-point loss log from scalar losses measured before and after training.

This is useful for any training routine that records a baseline loss at step 0 and another loss after steps updates. More detailed loops should use Curve or MetricHistory below.

structure Runtime.Training.Curve : Type

A single scalar curve over discrete training steps.

Use this when a training routine records one scalar repeatedly, such as training loss, validation loss, learning rate, or reward. Convert it to TrainLog for JSON persistence and widgets.

Curves use Arrays rather than tensors:

• curve lengths are runtime-dependent,
• curves are persisted as JSON for widgets, and
• typed tensors are reserved for fixed-shape model inputs/outputs.

• steps : Array Nat

  Step indices (e.g. update number).

• values : Array Float

  Scalar metric values aligned with steps.

@[instance_reducible]

instance Runtime.Training.instInhabitedCurve : Inhabited Curve

def Runtime.Training.Curve.push (c : Curve) (step : Nat) (value : Float) : Curve

Append one point (step, value) to a curve.

def Runtime.Training.Curve.toTrainLog (c : Curve) (title seriesName : String) (color : String := "#4e79a7") (notes : Array String := #[]) : TrainLog

Convert a single curve into a TrainLog with one series.

This matches the expectations of TorchLean's widgets (#train_log_file_view).

Multi-metric histories

Curve is perfect for a single scalar, but many training runs record several aligned metrics: train loss, validation loss, accuracy, learning rate, reward, and so on. MetricHistory stores that common table-shaped history and converts it to the stable TrainLog artifact consumed by JSON IO and widgets.

structure Runtime.Training.MetricHistory : Type

A multi-series scalar history aligned by step.

• steps : Array Nat

  Step indices shared by every series.

• series : Array Series

  Metric series. Each push appends one value to each series.

@[instance_reducible]

instance Runtime.Training.instInhabitedMetricHistory : Inhabited MetricHistory

def Runtime.Training.MetricHistory.empty (metrics : Array (String × String)) : MetricHistory

Construct an empty history from (metric name, color) pairs.

def Runtime.Training.MetricHistory.push (h : MetricHistory) (step : Nat) (values : Array Float) : MetricHistory

Append one row of metric values.

If values.size does not match series.size, the update is ignored. Callers that want a hard error can check sizes before calling.

def Runtime.Training.MetricHistory.toTrainLog (h : MetricHistory) (title : String) (notes : Array String := #[]) : TrainLog

Convert a multi-metric history into a stable TrainLog artifact.

structure Runtime.Training.ConfusionMatrix : Type

Confusion matrix for classification evaluation.

• counts : Array (Array Nat)

  Row-major counts: counts[i][j] means “true class i predicted as j”.

structure Runtime.Training.ExperimentLog : Type

A W&B-shaped local experiment artifact.

ExperimentLog is the richer authoring object. Use toTrainLog before writing JSON or rendering in widgets. The conversion stores metadata as structured notes so existing TrainLog consumers keep working without a second widget protocol.

• run : RunInfo

  Run metadata and config.

• history : MetricHistory

  Aligned scalar metrics over time.

• artifacts : Array Artifact

  Files produced or consumed by this run.

• notes : Array String

  Additional free-form notes.

@[instance_reducible]

instance Runtime.Training.instInhabitedExperimentLog : Inhabited ExperimentLog

Experiment-Tracker Helpers

def Runtime.Training.RunInfo.toNotes (run : RunInfo) : Array String

Render run metadata and config as stable notes inside a TrainLog.

def Runtime.Training.Artifact.toNote (a : Artifact) : String

Render an artifact reference as a stable note inside a TrainLog.

def Runtime.Training.ExperimentLog.init (run : RunInfo := { }) (metrics : Array (String × String) := #[]) : ExperimentLog

Start a local experiment with optional metadata.

def Runtime.Training.ExperimentLog.log (e : ExperimentLog) (step : Nat) (name : String) (value : Float) (color : String := "#4e79a7") : ExperimentLog

Record a scalar at a step. Consecutive writes at the same step share one row; writing the same metric again replaces its value. Unreported metrics use NaN, including earlier rows when a metric is first introduced.

def Runtime.Training.ExperimentLog.toTrainLog (e : ExperimentLog) (title : String := "") : TrainLog

Convert a rich experiment object into the stable widget/JSON TrainLog artifact.

Logging Destinations

Examples should make logging explicit. LogDestination.disabled is the local equivalent of wandb disabled; LogDestination.json path writes the standard TorchLean JSON artifact.

inductive Runtime.Training.LogDestination : Type

Where a training routine should send its log artifact.

• disabled : LogDestination

  Do not write a log artifact. Useful for tests, CI, and runs where metrics are printed only.

• json (path : System.FilePath) : LogDestination

  Write a local JSON artifact to the given path.

@[instance_reducible]

instance Runtime.Training.instInhabitedLogDestination : Inhabited LogDestination

@[instance_reducible]

instance Runtime.Training.instReprLogDestination : Repr LogDestination

def Runtime.Training.instReprLogDestination.repr : LogDestination → Nat → Std.Format

@[instance_reducible]

instance Runtime.Training.instBEqLogDestination : BEq LogDestination

def Runtime.Training.instBEqLogDestination.beq : LogDestination → LogDestination → Bool

@[instance_reducible]

instance Runtime.Training.instToStringLogDestination : ToString LogDestination

def Runtime.Training.LogDestination.isEnabled : LogDestination → Bool

Is logging enabled for this destination?

def Runtime.Training.LogDestination.path? : LogDestination → Option System.FilePath

Return the JSON path when this destination writes one.

def Runtime.Training.LogDestination.parse (raw : String) : LogDestination

Parse a CLI logging value.

Accepted disabled values are false, off, none, no, and disabled. Any other value is treated as a JSON path.

def Runtime.Training.LogDestination.resolve (default : LogDestination) (value? : Option String) : LogDestination

Resolve an optional CLI value, preserving default when no override is supplied.

JSON Codec

Training logs are often produced by executable examples and then rendered later by widgets. The codec below is stable and easy to inspect:

• finite floats are JSON numbers;
• non-finite floats are string sentinels ("NaN", "Infinity", "-Infinity");
• missing optional fields fall back to the same defaults as the Lean structures.

This artifact format keeps examples, tests, widgets, and external tooling speaking the same language.

Primitive arrays

def Runtime.Training.JsonCodec.floatToJson (x : Float) : Lean.Json

Encode finite metric values without losing precision to the default six-decimal formatter. Non-finite values use Lean's string sentinels; both signed zeros retain the historical JSON 0.

def Runtime.Training.JsonCodec.floatOfJsonE (field : String) (j : Lean.Json) : Except String Float

Decode a Float from JSON.

TrainLog files store finite floats as JSON numbers. The decoder also accepts Lean's non-finite string sentinels and numeric strings.

def Runtime.Training.JsonCodec.natArrayToJson (xs : Array Nat) : Lean.Json

Encode natural-number arrays used by logs and runtime artifacts.

def Runtime.Training.JsonCodec.natArrayOfJsonE (field : String) (j : Lean.Json) : Except String (Array Nat)

Decode natural-number arrays with field-aware errors.

def Runtime.Training.JsonCodec.stringArrayToJson (xs : Array String) : Lean.Json

Encode string-note arrays used by logs and runtime artifacts.

def Runtime.Training.JsonCodec.stringArrayOfJsonE (field : String) (j : Lean.Json) : Except String (Array String)

Decode string-note arrays with field-aware errors.

def Runtime.Training.JsonCodec.floatArrayToJson (xs : Array Float) : Lean.Json

Encode a float-valued metric series.

def Runtime.Training.JsonCodec.floatArrayOfJsonE (field : String) (j : Lean.Json) : Except String (Array Float)

Decode a float-valued metric series with field-aware errors.

def Runtime.Training.Series.toJson (s : Series) : Lean.Json

JSON encoding for one named metric series.

def Runtime.Training.Series.ofJsonE (j : Lean.Json) : Except String Series

JSON decoding for one named metric series.

def Runtime.Training.TrainLog.toJson (log : TrainLog) : Lean.Json

JSON encoding for the stable TrainLog artifact.

def Runtime.Training.TrainLog.ofJsonE (j : Lean.Json) : Except String TrainLog

JSON decoding for the stable TrainLog artifact.

def Runtime.Training.TrainLog.writeJson (path : System.FilePath) (log : TrainLog) (pretty : Bool := true) : IO Unit

Write a TrainLog as JSON to disk, creating parent directories if needed.

def Runtime.Training.TrainLog.readJson (path : System.FilePath) : IO TrainLog

Read a TrainLog from a JSON file.

structure Runtime.Training.ConfusionMatrix.Statistics : Type

Counts over every class, independent of any display limits.

• support : Array Nat

  Number of true examples per class (row totals).

• predicted : Array Nat

  Number of predictions per class (column totals).

• correct : Nat

  Number of correctly classified examples.

• total : Nat

  Total number of classified examples.

def Runtime.Training.ConfusionMatrix.statistics (cm : ConfusionMatrix) : Except String Statistics

Summarize a square confusion matrix, rejecting malformed row lengths.

def Runtime.Training.ConfusionMatrix.toJson (cm : ConfusionMatrix) : Lean.Json

JSON encoding for a classification confusion matrix.

def Runtime.Training.ConfusionMatrix.ofJsonE (j : Lean.Json) : Except String ConfusionMatrix

JSON decoding for a classification confusion matrix.

def Runtime.Training.ConfusionMatrix.writeJson (path : System.FilePath) (cm : ConfusionMatrix) (pretty : Bool := true) : IO Unit

Write a confusion matrix as JSON to disk, creating parent directories if needed.

def Runtime.Training.ConfusionMatrix.readJson (path : System.FilePath) : IO ConfusionMatrix

Read a confusion matrix from a JSON file.

def Runtime.Training.LogDestination.writeTrainLog (dest : LogDestination) (log : TrainLog) (pretty : Bool := true) : IO Unit

Write a TrainLog to this destination. Disabled destinations are a no-op.