TorchLean Trainer Runtime Options

Datasets, probes, runtime flag parsing, and per-training options for the public trainer facade.

structure TorchLean.Trainer.Dataset (σ τ : Shape) : Type 1

Runtime-polymorphic supervised dataset used by public trainer objects.

• build {α : Type} [Runtime.SemanticScalar α] [Runtime.Scalar α] : IO (Training.Dataset (SupervisedSample α σ τ))

  Materialize the dataset at the runtime-selected scalar type.

structure TorchLean.Trainer.Probe (σ : Shape) : Type 1

A small input probe printed before and after training.

• name : String

  Human-facing probe name.

• inputText : String

  Human-facing input description.

• input {α : Type} [Runtime.TensorScalar α] [Runtime.Scalar α] : Tensor.T α σ

  Runtime-polymorphic input tensor.

• expected : Option String

  Optional expected value shown beside the prediction.

def TorchLean.Trainer.Probe.vec2 (name : String) (x1 x2 : Float) (expected : Option String := none) : Probe (Shape.vec 2)

Two-coordinate vector probe, useful for small tabular regression examples.

def TorchLean.Trainer.Probe.ofFloatTensor {σ : Shape} (name : String) (x : Tensor.T Float σ) (inputText : String := "") (expected : Option String := none) : Probe σ

Probe built from a concrete Float tensor.

structure TorchLean.Trainer.RunConfigextends TorchLean.Trainer.RuntimeSettings : Type

Persistent runtime/training settings attached to a public trainer handle.

• optimizer : optim.Optimizer
• dtype : Runtime.DType
• backend : Runtime.Backend
• device : Runtime.Device
• fastKernels : Bool
• fastGpuMatmulPrecision : Runtime.Autograd.FastKernels.GpuMatmulPrecision

def TorchLean.Trainer.RunConfig.withDType (run : RunConfig) (dtype : Runtime.DType) : RunConfig

Override the scalar dtype for this run configuration.

def TorchLean.Trainer.RunConfig.withBackend (run : RunConfig) (backend : Runtime.Backend) : RunConfig

Override the execution backend for this run configuration.

def TorchLean.Trainer.RunConfig.withDevice (run : RunConfig) (device : Runtime.Device) : RunConfig

Override the execution device for this run configuration.

def TorchLean.Trainer.RunConfig.withFastKernels (run : RunConfig) (enabled : Bool := true) : RunConfig

Enable or disable runtime-only fast kernels for this run configuration.

def TorchLean.Trainer.RunConfig.withFastGpuMatmulPrecision (run : RunConfig) (precision : Runtime.Autograd.FastKernels.GpuMatmulPrecision) : RunConfig

Override CUDA matmul precision for fast kernels.

def TorchLean.Trainer.RunConfig.eager (run : RunConfig) : RunConfig

Use the eager runtime backend.

def TorchLean.Trainer.RunConfig.compiled (run : RunConfig) : RunConfig

Use the proof-compiled runtime backend.

def TorchLean.Trainer.RunConfig.cpu (run : RunConfig) : RunConfig

Run on CPU.

def TorchLean.Trainer.RunConfig.cuda (run : RunConfig) : RunConfig

Run on CUDA.

def TorchLean.Trainer.RunConfig.withOptions (run : RunConfig) (opts : Options) : RunConfig

Apply parsed runtime/device options to a persistent trainer run configuration.

def TorchLean.Trainer.RunConfig.fromOptions (opts : Options) (base : RunConfig := { }) : RunConfig

Build a run configuration from parsed runtime flags and trainer choices.

def TorchLean.Trainer.RunConfig.toOptions (run : RunConfig) : Options

Lower a public run configuration to the runtime Options record.

def TorchLean.Trainer.RunConfig.float32ModeArg : Floats.Float32Mode → String

CLI spelling for a Float32 runtime mode.

def TorchLean.Trainer.RunConfig.dtypeArgs : Runtime.DType → List String

CLI arguments that reproduce a public dtype choice.

def TorchLean.Trainer.RunConfig.backendArgs : Runtime.Backend → List String

CLI arguments that reproduce a public backend choice.

def TorchLean.Trainer.RunConfig.deviceArgs : Runtime.Device → List String

CLI arguments that reproduce a public device choice.

def TorchLean.Trainer.RunConfig.precisionArgs (p : Runtime.Autograd.FastKernels.GpuMatmulPrecision) : List String

CLI arguments that reproduce the CUDA matmul precision setting.

def TorchLean.Trainer.RunConfig.parseRuntimeArgs (args : List String) (base : RunConfig := { }) : Except String (RunConfig × List String)

Parse CLI runtime flags into persistent trainer run settings.

def TorchLean.Trainer.RunConfig.parseRuntimeArgsOrThrow (exeName : String) (args : List String) (base : RunConfig := { }) : IO RunConfig

Resolve runtime flags into a Trainer.RunConfig and reject unused trailing arguments.

def TorchLean.Trainer.RunConfig.toArgs (run : RunConfig) : List String

Lower this persistent run configuration to the standard runtime CLI flags.

def TorchLean.Trainer.Config.fromRunConfig {σ τ : Shape} (run : RunConfig) (task : Task σ τ := Task.regression) (seed : ℕ := 0) : Config σ τ

Build unified trainer construction options from an already parsed runtime configuration.

def TorchLean.Trainer.runConfig (opts : Options) (base : RunConfig := { }) : RunConfig

CLI-friendly public run configuration constructor.

def TorchLean.Trainer.Implementation.Regression.runConfig {σ τ : Shape} (trainer : Regression σ τ) : RunConfig

Runtime configuration carried by this trainer.

def TorchLean.Trainer.Implementation.CrossEntropy.runConfig {σ τ : Shape} (trainer : CrossEntropy σ τ) : RunConfig

Runtime configuration carried by this trainer.

def TorchLean.Trainer.Implementation.Custom.runConfig {σ τ : Shape} (trainer : Custom σ τ) : RunConfig

Runtime configuration carried by this trainer.

structure TorchLean.Trainer.TrainOptions : Type

Per-training-call options for the public trainer facade.

• steps : ℕ

  Number of optimizer updates.

• batchSize : ℕ

  Requested minibatch size for public training calls.

  Fixed-shape model-zoo trainers may already carry their batch axis in the model type. This field is still part of the public API so ordinary scripts can write the same record shape across simple tensor datasets, loader-backed examples, and future batched trainer paths.

• logEvery : ℕ

  Print step losses every logEvery updates; 0 disables stdout step logging.

• log : Training.LogDestination

  Optional TrainLog artifact destination. Use .disabled for stdout-only runs.

• title : String

  Title used when writing a TrainLog artifact.

• notes : Array String

  Free-form notes attached to the TrainLog artifact.

• loadParams? : Option System.FilePath

  Optional exact-bits parameter checkpoint loaded before training.

• saveParams? : Option System.FilePath

  Optional exact-bits parameter checkpoint written after training.

def TorchLean.Trainer.TrainOptions.forSteps (count : ℕ) : TrainOptions

Start training options with a fixed number of optimizer steps.

def TorchLean.Trainer.TrainOptions.withLogEvery (opts : TrainOptions) (logEvery : ℕ) : TrainOptions

Override stdout step logging cadence.

def TorchLean.Trainer.TrainOptions.withBatchSize (opts : TrainOptions) (batchSize : ℕ) : TrainOptions

Override the requested minibatch size.

def TorchLean.Trainer.TrainOptions.withLog (opts : TrainOptions) (log : Training.LogDestination) : TrainOptions

Override the training-log destination.

def TorchLean.Trainer.TrainOptions.disableLog (opts : TrainOptions) : TrainOptions

Disable TrainLog artifact writing for a training call that will write a richer custom artifact later.

def TorchLean.Trainer.TrainOptions.withTitle (opts : TrainOptions) (title : String) : TrainOptions

Override the training-log title.

def TorchLean.Trainer.TrainOptions.withNotes (opts : TrainOptions) (notes : Array String) : TrainOptions

Override the training-log notes.

def TorchLean.Trainer.TrainOptions.withLoadParams (opts : TrainOptions) (path : System.FilePath) : TrainOptions

Load an exact-bits parameter checkpoint before training.

def TorchLean.Trainer.TrainOptions.withSaveParams (opts : TrainOptions) (path : System.FilePath) : TrainOptions

Save an exact-bits parameter checkpoint after training.

def TorchLean.Trainer.TrainOptions.toTrainConfig (opts : TrainOptions) (optimizer : optim.Optimizer) : NN.API.TorchLean.Trainer.TrainConfig

Lower the public training options to the advanced runtime training config.

structure TorchLean.Trainer.ClassProbe (σ : Shape) : Type 1

A named classification input used for before/after prediction reporting.

• name : String

  Human-facing probe name.

• input {α : Type} [Runtime.TensorScalar α] [Runtime.Scalar α] : Tensor.T α σ

  Runtime-polymorphic input tensor.

• expected : ℕ

  Expected class index, printed beside the prediction.

def TorchLean.Trainer.ClassProbe.toBatchedProbe {σ : Shape} (batch : ℕ) (probe : ClassProbe σ) : Probe (Spec.Shape.dim batch σ)

Convert a single-example class probe into the batched tensor probe used by trainer.train.