Core training helpers

These are small, reusable utilities that keep training scripts short and readable. They are pure and local.

def Runtime.Autograd.Train.tagError (tag msg : String) : String

Prefix an error message with a caller-provided tag.

This is used throughout the training helpers to keep error messages readable when multiple subsystems can fail (tape execution, dataset loading, shape checks, etc.).

Typed extraction helpers

The autograd engine stores values and gradients as Spec.SomeTensor (shape tag + tensor). These helpers check shapes and give you back a typed tensor or a scalar value.

def Runtime.Autograd.Train.requireGradTensor {a : Type} [TorchLean.Storage a] {s : Spec.Shape} (tag : String) (grads : Std.HashMap ℕ (Spec.SomeTensor a)) (id : ℕ) : Result (TorchLean.Tensor a s)

Read a typed gradient tensor Tensor a s from a gradient map keyed by node id.

The eager tape engine stores gradients in a shape-erased form (Spec.SomeTensor a), so this helper performs the dynamic shape check and returns a typed tensor on success.

def Runtime.Autograd.Train.requireValueTensor {a : Type} [TorchLean.Storage a] {s : Spec.Shape} (tag : String) (t : Tape a) (id : ℕ) : Result (TorchLean.Tensor a s)

Read a typed forward value Tensor a s from a tape node id.

This is the value-side analogue of requireGradTensor: it checks the shape stored in the packed tensor before recovering a statically shaped value.

def Runtime.Autograd.Train.requireScalarValue {a : Type} [TorchLean.Storage a] (tag : String) (t : Tape a) (id : ℕ) : Result a

Read a scalar forward value from a tape node id.

This is a common pattern in training scripts where the loss is a scalar node.

SGD update helper

This is a small tensor-level update used by many tests.