Trainer Runtime Flags

Command-line parsing for Trainer.RunConfig. Import this module in applications that accept training runtime settings. The flags are --arithmetic, --execution, --device, and --show-backend; everything else is returned to the caller.

def TorchLean.CLI.Trainer.parse (arguments : List String) (base : Trainer.RunConfig := { }) : Except String (Trainer.RunConfig × List String)

Parse runtime flags over base, preserving unselected defaults and returning unused arguments.

An explicit device flag clears a programmatic backend profile so it cannot override the CLI choice.

def TorchLean.CLI.Trainer.parseCommandLine (exeName : String) (arguments : List String) (base : Trainer.RunConfig := { }) : IO Trainer.RunConfig

Parse a complete command line, raising an IO.userError for invalid or unused arguments.

def TorchLean.CLI.Trainer.cliArguments (run : Trainer.RunConfig) : List String

Render a run configuration as the command-line arguments parse accepts.

def TorchLean.CLI.Training.RunOptions.trainOptions (runOptions : RunOptions) (enableLog : Bool := true) (logEvery : ℕ := 0) (logTitle : String := "Training") (logNotes : Array String := #[]) : Trainer.TrainOptions

Training options consumed by Trainer.train.

def TorchLean.CLI.Training.OptimizerOptions.trainOptions (optimizerOptions : OptimizerOptions) (enableLog : Bool := true) (logEvery : ℕ := 0) (logTitle : String := "Training") (logNotes : Array String := #[]) : Trainer.TrainOptions

Training options consumed by Trainer.train.