Runnable Example Training Support

Logging, runtime, and fixed-sample training helpers used by the runnable model examples.

def NN.Examples.Support.cudaMemoryNote (runtime : TorchLean.Runtime.Config) (steps requested : ℕ) : String

Training-log note recording the selected CUDA allocator-reporting cadence.

Shared CLI and logging names for the built-in runnable examples.

These are public so examples can stay short and readable. They live under Support; ordinary library code should usually use Trainer, Data, and optim directly.

def NN.Examples.Support.trainLogPath (stem : String) : System.FilePath

Standard location for a runnable example's training log under data/examples.

def NN.Examples.Support.deviceNote (runtime : TorchLean.Runtime.Config) : String

device=... note string used by example logs.

def NN.Examples.Support.bannerWithDevice (exeName desc : String) (runtime : TorchLean.Runtime.Config) : String

Example banner with the executable name, a short description, and the selected device.

def NN.Examples.Support.bannerWithDeviceDetails (exeName desc details : String) (runtime : TorchLean.Runtime.Config) : String

Two-line example banner: a headline with the selected device, then one detail line.

def NN.Examples.Support.check (exeName msg : String) (b : Bool) : IO Unit

Fail with a contextual error when an executable model check is false.