Shared Model Training Commands

Example-side command runners for built-in model-zoo entries.

The trainer API provides Trainer.new, trainer.train, and trained prediction handles. This file owns repository command plumbing: parse model-zoo flags, check local files, run training, and print the standard summary.

def NN.Examples.Models.TrainCommand.runParsedWith {φ ρ : Type} (exeName : String) (args : List String) (parseFlags : List String → Except String (φ × List String)) (banner : Runtime.Autograd.Torch.Options → String) (train : Runtime.Autograd.Torch.Options → φ → IO ρ) (finish : Runtime.Autograd.Torch.Options → φ → ρ → IO Unit) : IO UInt32

Run one parsed model-training command and finish with access to runtime flags and result.

def NN.Examples.Models.TrainCommand.runParsed {φ ρ : Type} (exeName : String) (args : List String) (parseFlags : List String → Except String (φ × List String)) (banner : Runtime.Autograd.Torch.Options → String) (train : Runtime.Autograd.Torch.Options → φ → IO ρ) (print : ρ → IO Unit) : IO UInt32

Run one parsed model-training command when the final printer only needs the trained result.

def NN.Examples.Models.TrainCommand.regressionCsv {σ τ : Spec.Shape} (exeName : String) (args : List String) (defaultCsv defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) (banner : Runtime.Autograd.Torch.Options → String) (train : Runtime.Autograd.Torch.Options → ModelZoo.CsvTrainFlags → IO (TorchLean.Trainer.TrainResult σ τ)) : IO UInt32

CSV-backed regression command using the public trainer API.

def NN.Examples.Models.TrainCommand.classificationNpy (exeName : String) (args : List String) (parseFlags : List String → Except String (ModelZoo.NpyModelTrainFlags × List String)) (banner : Runtime.Autograd.Torch.Options → String) (train : Runtime.Autograd.Torch.Options → ModelZoo.NpyModelTrainFlags → IO TorchLean.Trainer.TrainSummary) : IO UInt32

NPY-backed classifier command using the public trainer API.

def NN.Examples.Models.TrainCommand.regressionNpy {σ τ : Spec.Shape} (exeName : String) (args : List String) (parseFlags : List String → Except String (ModelZoo.NpyModelTrainFlags × List String)) (banner : Runtime.Autograd.Torch.Options → String) (train : Runtime.Autograd.Torch.Options → ModelZoo.NpyModelTrainFlags → IO (TorchLean.Trainer.TrainResult σ τ)) : IO UInt32

NPY-backed regression command using the public trainer API.

def NN.Examples.Models.TrainCommand.forecastWindow {σ τ : Spec.Shape} (exeName : String) (args : List String) (parseFlags : List String → Except String (ModelZoo.ForecastWindowModelTrainFlags × List String)) (banner : Runtime.Autograd.Torch.Options → String) (train : Runtime.Autograd.Torch.Options → ModelZoo.ForecastWindowModelTrainFlags → IO (TorchLean.Trainer.TrainResult σ τ)) : IO UInt32

Forecast-window regression command using the public trainer API.

structure NN.Examples.Models.TrainCommand.Config (δ : Type) : Type

Shared runner for the normal lake exe torchlean ... training commands.

This is the common path for examples that load data, train once, and print the standard report. A model file should only define its own option record when it genuinely does more than training, for example text generation, probe evaluation, or a custom curriculum.

• exeName : String

  CLI subcommand name, for example torchlean rnn.

• defaultLogJson : System.FilePath

  Default JSON log path used when --log is omitted.

• defaultSteps : ℕ

  Default number of optimizer steps when --steps is omitted.

• description : String

  Model description used in banners.

• dataOptions : List String

  Command-specific data flags, rendered by --help.

• parseData : List String → Except String (δ × List String)

  Parse data flags, then leave device/training flags for the shared parser.

• train : Runtime.Autograd.Torch.Options → δ → TorchLean.CLI.Training.RunOptions → IO Unit

  Run the actual training body after data, device, and training flags have been parsed.

def NN.Examples.Models.TrainCommand.usage {δ : Type} (cfg : Config δ) : String

Usage text for model examples using the shared runner.

def NN.Examples.Models.TrainCommand.run {δ : Type} (cfg : Config δ) (args : List String) : IO UInt32

Run a public model-training command.