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 deliberately small:

• 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.

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 intentionally local-first. The shape mirrors the small useful 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

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

@[implicit_reducible]

instance Runtime.Training.instInhabitedConfigEntry : Inhabited ConfigEntry

def Runtime.Training.instInhabitedConfigEntry.default : 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 human-readable description.

def Runtime.Training.instInhabitedArtifact.default : Artifact

@[implicit_reducible]

instance Runtime.Training.instInhabitedArtifact : Inhabited Artifact

structure Runtime.Training.RunInfo : Type

Run metadata for a local experiment.

This is deliberately close to the mental model of W&B (project, name, group, tags, config), but it remains a plain Lean value and does not perform 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.

@[implicit_reducible]

instance Runtime.Training.instInhabitedRunInfo : Inhabited RunInfo

def Runtime.Training.instInhabitedRunInfo.default : 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.

def Runtime.Training.instInhabitedSeries.default : Series

@[implicit_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.beforeAfterLoss (title : String) (steps : Nat) (loss0 loss1 : Float) (notes : Array String := #[]) (color : String := "#4e79a7") : TrainLog

Build a two-point loss log from an initial and final scalar loss.

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.

We intentionally store curves as Arrays (not 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.

@[implicit_reducible]

instance Runtime.Training.instInhabitedCurve : Inhabited Curve

def Runtime.Training.instInhabitedCurve.default : 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.

@[implicit_reducible]

instance Runtime.Training.instInhabitedMetricHistory : Inhabited MetricHistory

def Runtime.Training.instInhabitedMetricHistory.default : 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. This keeps the function total and avoids manufacturing malformed logs; 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.

@[implicit_reducible]

instance Runtime.Training.instInhabitedExperimentLog : Inhabited ExperimentLog

def Runtime.Training.instInhabitedExperimentLog.default : 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

Append one scalar metric. New metric names are added lazily with a default color.

def Runtime.Training.ExperimentLog.logRow (e : ExperimentLog) (step : Nat) (values : Array Float) : ExperimentLog

Append one aligned row of metrics to an experiment.

def Runtime.Training.ExperimentLog.addArtifact (e : ExperimentLog) (artifact : Artifact) : ExperimentLog

Attach a local file artifact to the run.

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 lightweight tests or CI runs.

• json (path : System.FilePath) : LogDestination

  Write a local JSON artifact to the given path.

def Runtime.Training.instInhabitedLogDestination.default : LogDestination

@[implicit_reducible]

instance Runtime.Training.instInhabitedLogDestination : Inhabited LogDestination

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

@[implicit_reducible]

instance Runtime.Training.instReprLogDestination : Repr 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.pathD (dest : LogDestination) (defaultPath : System.FilePath) : System.FilePath

Return the JSON path, falling back to defaultPath when logging is disabled.

def Runtime.Training.LogDestination.parseValue (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.parse? (defaultPath : System.FilePath) (raw? : Option String) : LogDestination

Parse an optional CLI value, using the default JSON path when no value is supplied.

JSON Codec

Training logs are often produced by executable examples and then rendered later by widgets. The codec below is intentionally stable and human-readable:

• 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 is not intended to be a high-throughput experiment tracker. It is a small artifact format that keeps examples, tests, widgets, and external tooling speaking the same language.

Primitive arrays

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

Encode a Float as JSON: a number when finite, otherwise Lean's standard string sentinel.

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

Decode a Float from JSON.

We accept JSON numbers, Lean's non-finite string sentinels, and numeric strings for backward compatibility with generated artifacts.

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

Encode natural-number arrays used by logs and lightweight 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 lightweight 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.

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.

def Runtime.Training.LogDestination.writeExperimentLog (dest : LogDestination) (log : ExperimentLog) (title : String := "") (pretty : Bool := true) : IO Unit

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