Model-Zoo Training Support

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

def NN.Examples.ModelZoo.effectiveCudaMemWatch (opts : Runtime.Autograd.Torch.Options) (steps requested : ℕ) : ℕ

Resolve the CUDA allocator-reporting cadence for a model-zoo run.

def NN.Examples.ModelZoo.cudaMemWatchNote (opts : Runtime.Autograd.Torch.Options) (steps requested : ℕ) : String

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

def NN.Examples.ModelZoo.reportCudaMemWatch (opts : Runtime.Autograd.Torch.Options) (watchEvery totalSteps completed : ℕ) (state? : Option TorchLean.Trainer.Manual.CudaMemWatchState) : IO (Option TorchLean.Trainer.Manual.CudaMemWatchState)

Sample and report CUDA allocator state when the selected cadence is reached.

def NN.Examples.ModelZoo.shouldLogStep (every completed : ℕ) : Bool

Return whether a completed model-zoo step should emit a periodic report.

def NN.Examples.ModelZoo.printCurveLossSummary (steps : ℕ) (curve : Runtime.Training.Curve) : IO Unit

Print the first and last losses recorded by a model-zoo training curve.

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

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

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

Standard location for a model-example training log under data/model_zoo.

def NN.Examples.ModelZoo.orThrow {α : Type} (exeName : String) (result : Except String α) : IO α

Lift a parser result into IO, prefixing failures with the executable name.

def NN.Examples.ModelZoo.deviceName (opts : Runtime.Autograd.Torch.Options) : String

Runtime device label used by example banners and notes.

def NN.Examples.ModelZoo.deviceNote (opts : Runtime.Autograd.Torch.Options) : String

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

def NN.Examples.ModelZoo.bannerWithDevice (exeName desc : String) (opts : Runtime.Autograd.Torch.Options) : String

Model-zoo banner with the executable name, a short description, and the selected device.

def NN.Examples.ModelZoo.bannerWithDeviceDetails (exeName desc details : String) (opts : Runtime.Autograd.Torch.Options) : String

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

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

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

def NN.Examples.ModelZoo.writeBeforeAfterLossLogPath (path : System.FilePath) (title : String) (steps : ℕ) (beforeLoss afterLoss : Float) (notes : Array String := #[]) : IO Unit

Write a before-and-after loss comparison to a JSON file.

def NN.Examples.ModelZoo.writeBeforeAfterLossLog (dest : Runtime.Training.LogDestination) (title : String) (steps : ℕ) (beforeLoss afterLoss : Float) (notes : Array String := #[]) : IO Unit

Write a before-and-after loss comparison to the selected logging destination.

def NN.Examples.ModelZoo.writeCurveLog (dest : Runtime.Training.LogDestination) (title : String) (curve : Runtime.Training.Curve) (seriesName : String := "loss") (notes : Array String := #[]) : IO Unit

Write one scalar curve to the selected logging destination.

def NN.Examples.ModelZoo.writeCurveTrainLog (dest : Runtime.Training.LogDestination) (title : String) (curve : Runtime.Training.Curve) (seriesName : String) (color : String := "#4e79a7") (notes : Array String := #[]) : IO Unit

Write a single-curve training log with an explicit series color.

Use this when a command already has a Training.Curve and wants a TrainLog instead of the default "loss" curve writer.

def NN.Examples.ModelZoo.writeMetricHistoryLog (dest : Runtime.Training.LogDestination) (title : String) (history : Runtime.Training.MetricHistory) (notes : Array String := #[]) : IO Unit

Write a multi-series metric history as a TrainLog artifact.

Use this when a command has a Training.MetricHistory with named, colored series and wants to write the usual TrainLog artifact without repeating the conversion code in every example.

def NN.Examples.ModelZoo.writeTrainLogPath (path : System.FilePath) (log : Runtime.Training.TrainLog) : IO Unit

Write a prepared training log to a JSON file.

def NN.Examples.ModelZoo.writeTrainLog (dest : Runtime.Training.LogDestination) (log : Runtime.Training.TrainLog) : IO Unit

Write a prepared training log to the selected destination.

def NN.Examples.ModelZoo.trainFixedCurveFloat {σ τ : Spec.Shape} (mkModel : TorchLean.nn.M (TorchLean.nn.Sequential σ τ)) (mkModuleDef : (model : TorchLean.nn.Sequential σ τ) → Runtime.Autograd.TorchLean.ScalarModuleDef (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model) [σ, τ]) (mkOptim : (paramShapes : List Spec.Shape) → Runtime.Autograd.TorchLean.Optimizer Float paramShapes) (opts : Runtime.Autograd.Torch.Options) (sample : TorchLean.SupervisedSample Float σ τ) (steps : ℕ) (cudaMemWatch : ℕ := 0) : IO Runtime.Training.Curve

Fixed-sample run specialized to Float, returning a full per-step curve.