Training Application Commands

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

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 and print 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.

• defaultLr : 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.trainingFlags (defaultSteps? : Option ℕ := none) (defaultLr? : Option Float := none) : Array String

The training flags CLI.Training.OptimizerOptions.parse accepts, with defaults when given.

def TorchLean.CLI.Training.Command.helpText (exeName : String) (dataOptions : Array String) (trainingOptions : Array String := trainingFlags) (description? : Option String := none) : String

Help text for a training command: its usage line, its data flags, the training flags, and the runtime flags the shared runner parses. Every training command prints this layout.

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.