Training Application Commands

Compose an application-specific data parser and training callback with common CLI options.

def TorchLean.CLI.Training.Command.runParsedWith {φ ρ : Type} (exeName : String) (args : List String) (parseFlags : List String → Except String (φ × List String)) (banner : Runtime.Config → String) (train : Runtime.Config → φ → IO ρ) (finish : Runtime.Config → φ → ρ → IO Unit) (usage? : Option String := none) : IO UInt32

Run a parsed training command and finish with access to runtime flags and the result.

def TorchLean.CLI.Training.Command.runParsed {φ ρ : Type} (exeName : String) (args : List String) (parseFlags : List String → Except String (φ × List String)) (banner : Runtime.Config → String) (train : Runtime.Config → φ → IO ρ) (print : ρ → IO Unit) (usage? : Option String := none) : IO UInt32

Run a parsed training command whose final printer only needs the trained result.

structure TorchLean.CLI.Training.Command.Config (δ : Type) : Type

Shared command runner for training applications with a caller-defined data parser.

Applications supply their data selection and training callback. The runner owns common flags, help output, and runtime selection.

• exeName : String

  CLI subcommand name, for example rnn.

• defaultLogPath : System.FilePath

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

• defaultSteps : ℕ

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

• defaultLearningRate : Float

  Learning rate used when --lr is omitted.

• description : String

  Model description used in banners.

• dataOptions : Array 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.Config → δ → OptimizerOptions → IO Unit

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

def TorchLean.CLI.Training.Command.usage {δ : Type} (config : Config δ) : String

Usage text for training applications using the shared runner.

def TorchLean.CLI.Training.Command.run {δ : Type} (config : Config δ) (args : List String) : IO UInt32

Run a public native-arithmetic training command.