Training Options

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

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

Supervised dataset that can be materialized at the trainer's selected scalar type.

• build {α : Type} [Context α] [Runtime.FromFloat α] : IO (Runtime.Autograd.Train.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} [Context α] [Runtime.FromFloat α] : Tensor.T α σ

  Runtime-polymorphic input tensor.

• expected : Option String

  Optional expected value shown beside the prediction.

def TorchLean.Trainer.Probe.point (name : String) (x y : Float) (expected : Option String := none) : Probe (Spec.Shape.dim 2 Shape.scalar)

Two-coordinate vector probe 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

Runtime and optimizer settings stored with a trainer.

• optimizer : optim.Optimizer
• dtype : Runtime.DType
• backend : Runtime.Backend
• executionProfile : NN.Backend.BackendProfile
• showBackend : Bool

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) : Except String RunConfig

Override the execution device using a maintained backend profile.

def TorchLean.Trainer.RunConfig.withBackendProfile (run : RunConfig) (profile : NN.Backend.BackendProfile) : RunConfig

Select a complete backend contract profile.

The profile carries the device, provider preference, assurance policy, VJP ownership, and capsule registry together. It can select, for example, LibTorch forward execution with a TorchLean-owned backward pass.

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

Enable or disable first-use backend capsule reporting.

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

Convert a 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 dtype choice.

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

CLI arguments that reproduce a backend choice.

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

CLI arguments that reproduce a device choice.

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 trainer options from an already parsed runtime configuration.

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

Build a run configuration from parsed runtime options.

def TorchLean.Trainer.Implementation.withReadableRuntime {β : Type} (dtype : Runtime.DType) (k : {α : Type} → [Context α] → [DecidableEq Shape] → [ToString α] → [Runtime.FromFloat α] → [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] → IO β) : IO (Except String β)

Run a callback under a runtime dtype that can also be read back to host Float tensors.

Trainer methods return ordinary Float predictions for display and downstream scripts, even when the model itself runs under an executable scalar such as IEEE32Exec. This dispatcher carries the extra scalar-readback evidence that DType.withRuntime intentionally does not require.

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 trainer API.

• steps : ℕ

  Number of optimizer updates.

• batchSize : ℕ

  Number of dataset items included in one optimizer update.

  For an ordinary sample dataset, each item is one example. A dataset made by Data.batchDataset already stores fixed-size tensor minibatches as its items; the usual vectorized path therefore keeps this option at 1. Values above one accumulate gradients from several such items before updating.

• scheduler : Option Scheduler.Config

  Optional learning-rate schedule, indexed by completed optimizer updates.

• logEvery : ℕ

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

• cudaMemWatch : ℕ

  Sample CUDA allocator state every this many completed updates; 0 disables sampling.

• 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.withCudaMemWatch (opts : TrainOptions) (cudaMemWatch : ℕ) : TrainOptions

Override the CUDA allocator sampling cadence.

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

Override the requested minibatch size.

def TorchLean.Trainer.TrainOptions.withScheduler (opts : TrainOptions) (scheduler : Scheduler.Config) : TrainOptions

Apply a learning-rate schedule during this training call.

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

Run with the optimizer's fixed learning rate.

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) : Manual.TrainConfig

Lower the public training options to the manual 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} [Context α] [Runtime.FromFloat α] : 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.