Shared Model Training Commands

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

The public trainer facade owns 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 TorchLean.Trainer.Command.runParsedWith {φ ρ : Type} (exeName : String) (args : List String) (parseFlags : List String → Except String (φ × List String)) (banner : Options → String) (train : Options → φ → IO ρ) (finish : Options → φ → ρ → IO Unit) : IO UInt32

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

def TorchLean.Trainer.Command.runParsed {φ ρ : Type} (exeName : String) (args : List String) (parseFlags : List String → Except String (φ × List String)) (banner : Options → String) (train : Options → φ → IO ρ) (print : ρ → IO Unit) : IO UInt32

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

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

CSV-backed regression command using the public trainer API.

def TorchLean.Trainer.Command.classificationNpy (exeName : String) (args : List String) (parseFlags : List String → Except String (ModelZoo.NpyModelTrainFlags × List String)) (banner : Options → String) (train : Options → ModelZoo.NpyModelTrainFlags → IO TrainSummary) : IO UInt32

NPY-backed classifier command using the public trainer API.

def TorchLean.Trainer.Command.regressionNpy {σ τ : Shape} (exeName : String) (args : List String) (parseFlags : List String → Except String (ModelZoo.NpyModelTrainFlags × List String)) (banner : Options → String) (train : Options → ModelZoo.NpyModelTrainFlags → IO (TrainResult σ τ)) : IO UInt32

NPY-backed regression command using the public trainer API.

def TorchLean.Trainer.Command.forecastWindow {σ τ : Shape} (exeName : String) (args : List String) (parseFlags : List String → Except String (ModelZoo.ForecastWindowModelTrainFlags × List String)) (banner : Options → String) (train : Options → ModelZoo.ForecastWindowModelTrainFlags → IO (TrainResult σ τ)) : IO UInt32

Forecast-window regression command using the public trainer API.

structure TorchLean.Trainer.Command.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.

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

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

• train : Options → δ → ModelZoo.LoggedTrainFlags → IO Unit

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

def TorchLean.Trainer.Command.usage {δ : Type} (cfg : Config δ) : String

Usage text for shared Trainer.Command.run model examples.

def TorchLean.Trainer.Command.run {δ : Type} (cfg : Config δ) (args : List String) : IO UInt32

Run a public model-training command.