TorchLean Model-Zoo Facade

Shared flags, logs, banners, paths, and runtime operations for built-in model-zoo examples.

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

These are public because examples should read like TorchLean programs. They stay under ModelZoo; ordinary library users should prefer Trainer, Data, and optim directly.

@[reducible, inline]

abbrev TorchLean.ModelZoo.TrainFlags : Type

Training flags shared by runnable model examples.

This covers the knobs almost every example needs: --steps, --log, CUDA memory watching, and --lr. Model files should reuse this record and add only flags that change that model's actual behavior, such as text generation settings or evaluation probes.

@[reducible, inline]

abbrev TorchLean.ModelZoo.SeededTrainFlags : Type

Model-training flags plus an RNG/data-order seed.

Use this when the command needs reproducible initialization, synthetic data, or shuffled row order in addition to the standard training flags.

@[reducible, inline]

abbrev TorchLean.ModelZoo.LoggedTrainFlags : Type

Common CLI result for training commands that accept --steps, --batch-size, and --log.

@[reducible, inline]

abbrev TorchLean.ModelZoo.CsvTrainFlags : Type

Common arguments for a model command that reads one supervised CSV.

@[reducible, inline]

abbrev TorchLean.ModelZoo.WindowOptions : Type

Shared corpus-window or training-window count used by finite cyclic examples.

@[reducible, inline]

abbrev TorchLean.ModelZoo.WindowOptions.parse (exeName : String) (args : List String) (defaultWindows : ℕ) : Except String (NN.API.Common.WindowOptions × List String)

Parse the shared --windows flag.

The model decides how to use the windows; this helper just keeps the flag spelling and positivity check consistent.

@[reducible, inline]

abbrev TorchLean.ModelZoo.CheckpointOptions : Type

Optional parameter-checkpoint load/save paths shared by runnable model commands.

@[reducible, inline]

abbrev TorchLean.ModelZoo.CheckpointOptions.parse (args : List String) : Except String (NN.API.Common.CheckpointOptions × List String)

Parse the shared --load-params / --save-params flags.

@[reducible, inline]

abbrev TorchLean.ModelZoo.DiffusionScheduleFlags : Type

Diffusion schedule knobs shared by model-zoo diffusion commands.

@[reducible, inline]

abbrev TorchLean.ModelZoo.DiffusionScheduleFlags.parse (args : List String) : Except String (NN.API.Common.DiffusionScheduleFlags × List String)

Parse shared diffusion schedule flags: --T, --beta-start, and --beta-end.

@[reducible, inline]

abbrev TorchLean.ModelZoo.DiffusionScheduleFlags.trainLogNotes (cfg : NN.API.Common.DiffusionScheduleFlags) : Array String

Standard TrainLog metadata for a diffusion schedule.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ImageArtifactFlags : Type

Optional image artifacts emitted by image-generation or reconstruction commands.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ImageArtifactFlags.parse (args : List String) : Except String (NN.API.Common.ImageArtifactFlags × List String)

Parse shared image artifact flags for generation/reconstruction commands.

This only parses artifact paths and the optional reconstruction timestep. The model still decides which images it can write.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ImageArtifactFlags.trainLogNotes (cfg : NN.API.Common.ImageArtifactFlags) : Array String

Standard TrainLog metadata for requested image artifacts.

@[reducible, inline]

abbrev TorchLean.ModelZoo.PairedNpyEvalFlags : Type

Common paired-NPY dataset flags for scientific supervised examples.

This shape is for commands that train on one (x,y) tensor pair and evaluate/report on a held-out pair. The model file supplies the tensor shapes and file defaults.

@[reducible, inline]

abbrev TorchLean.ModelZoo.PairedNpyEvalFlags.parse (args : List String) (defaultTrainX defaultTrainY defaultTestX defaultTestY : System.FilePath) (defaultTrainRows defaultTestRows : ℕ) : Except String (NN.API.Common.PairedNpyEvalFlags × List String)

Parse common train/test paired-NPY flags.

Commands supply their default paths and row counts. This parser keeps the repeated --train-rows, --test-rows, --eval-rows, --x, --y, --test-x, and --test-y flags in one place.

@[reducible, inline]

abbrev TorchLean.ModelZoo.PairedNpyEvalFlags.trainLogNotes (cfg : NN.API.Common.PairedNpyEvalFlags) : Array String

Standard TrainLog metadata for paired train/test NPY tensors.

@[reducible, inline]

abbrev TorchLean.ModelZoo.CsvArtifactFlags : Type

Optional CSV artifact path for commands that emit one tabular diagnostic.

@[reducible, inline]

abbrev TorchLean.ModelZoo.CsvArtifactFlags.parse (args : List String) (defaultPlotCsv : System.FilePath) : Except String (NN.API.Common.CsvArtifactFlags × List String)

Parse the shared optional --plot-csv artifact path.

@[reducible, inline]

abbrev TorchLean.ModelZoo.NpyDataFlags : Type

Generic NPY-backed labeled dataset flags.

Examples provide default paths and data-preparation hints. The repeated flags are --seed, --n-total, --x, and --y.

@[reducible, inline]

abbrev TorchLean.ModelZoo.NpyDataFlags.parse (args : List String) (defaultX defaultY : System.FilePath) (defaultRows : ℕ) : Except String (NN.API.Common.NpyDataFlags × List String)

Parse the standard --seed, --n-total, --x, and --y flags for NPY-backed datasets.

Examples provide dataset-specific defaults; this parser keeps the repeated NPY dataset flags consistent.

@[reducible, inline]

abbrev TorchLean.ModelZoo.NpyDataFlags.trainLogNotes (cfg : NN.API.Common.NpyDataFlags) (datasetName : String) : Array String

Standard TrainLog metadata for an NPY-backed dataset branch.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ImageDatasetChoice : Type

Built-in image dataset branches shared by image-model commands.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ImageDatasetChoice.parse (args : List String) : Except String (NN.API.Common.ImageDatasetChoice × List String)

Parse --dataset, --cifar10, and --imagenet64, rejecting ambiguous selectors.

@[reducible, inline]

abbrev TorchLean.ModelZoo.NpyLoggedTrainFlags : Type

Common arguments for a fixed-sample command backed by supervised .npy arrays.

def TorchLean.ModelZoo.NpyLoggedTrainFlags.parse (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ) (parseData : List String → Except String (NpyDataFlags × List String)) : Except String NpyLoggedTrainFlags

Parse a supervised NPY dataset, logged training flags, and require that no command-specific arguments remain.

Dataset-specific commands provide parseData, which owns defaults such as CIFAR or ImageNet paths; this helper keeps the reusable "NPY data + logged TrainLog" path in one place.

@[reducible, inline]

abbrev TorchLean.ModelZoo.NpyModelTrainFlags : Type

Common arguments for a model-training command backed by supervised .npy arrays.

def TorchLean.ModelZoo.NpyModelTrainFlags.parse (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) (parseData : List String → Except String (NpyDataFlags × List String)) : Except String (NpyModelTrainFlags × List String)

Parse a supervised NPY dataset and standard model-training flags.

The remaining arguments are returned so callers can still pass runtime/backend flags through a higher-level runner.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ForecastWindowDataFlags : Type

Shared forecasting-window data flags: paths, window count, report offset, and seed.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ForecastWindowDataFlags.trainLogNotes (cfg : NN.API.Common.ForecastWindowDataFlags) : Array String

Standard TrainLog metadata for forecasting-window datasets.

@[reducible, inline]

abbrev TorchLean.ModelZoo.ForecastWindowModelTrainFlags : Type

Common arguments for forecasting-window model-training commands.

def TorchLean.ModelZoo.ForecastWindowModelTrainFlags.parse (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 100) (defaultLr : Float := 1e-2) (parseData : List String → Except String (ForecastWindowDataFlags × List String)) : Except String (ForecastWindowModelTrainFlags × List String)

Parse forecasting-window data flags plus standard model-training flags.

The data parser comes from the caller because file defaults often depend on a dataset directory or a preparation script.

@[reducible, inline]

abbrev TorchLean.ModelZoo.trainLogPath (stem : String) : System.FilePath

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

@[reducible, inline]

abbrev TorchLean.ModelZoo.requirePositiveNatFlag (exeName flag : String) (value : ℕ) : Except String Unit

Validate that a natural-number CLI flag is positive.

@[reducible, inline]

abbrev TorchLean.ModelZoo.resolvePositiveNatFlag (exeName flag : String) (value? : Option ℕ) (default : ℕ) : Except String ℕ

Resolve an optional natural-number CLI flag against a default and require that the result is strictly positive.

Example parsers use this helper for the common "optional flag + default + positivity check" case instead of restating the same getD / requirePositiveNatFlag sequence.

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

Convert an Except String α into an IO α, raising a tagged userError on failure.

This is handy in main functions where we want the process to exit with a readable message.

@[reducible, inline]

abbrev TorchLean.ModelZoo.runFloat (exeName : String) (args : List String) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) : IO UInt32

Run an executable on the concrete Float runtime path.

We use this for runnable training commands that produce Float-valued artifacts: CPU/CUDA eager execution, native kernels, and JSON loss curves. Commands that need to expose another scalar backend can use runAnyOrFloat.

@[reducible, inline]

abbrev TorchLean.ModelZoo.runAnyOrFloat (exeName : String) (args : List String) (preferFloat : List String → Bool) (banner : Runtime.Autograd.Torch.Options → String) (anyK : {α : Type} → [NN.API.Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [NN.API.Runtime.Scalar α] → (Float → α) → Runtime.Autograd.Torch.Options → List String → IO Unit) (floatK : Runtime.Autograd.Torch.Options → List String → IO Unit) : IO UInt32

Run an executable with the standard TorchLean runtime parser, using the polymorphic scalar path by default and switching to the Float path when requested.

This is the common shape for public examples that support all executable scalar backends, but need the Float path for CUDA bridges, decoded reports, or JSON artifacts whose metrics are stored as Float.

@[reducible, inline]

abbrev TorchLean.ModelZoo.runAnyOrFloatNoCast (exeName : String) (args : List String) (preferFloat : List String → Bool) (banner : Runtime.Autograd.Torch.Options → String) (anyK : {α : Type} → [NN.API.Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [NN.API.Runtime.Scalar α] → Runtime.Autograd.Torch.Options → List String → IO Unit) (floatK : Runtime.Autograd.Torch.Options → List String → IO Unit) : IO UInt32

Run an executable on either the selected scalar backend or the concrete Float path when the generic branch does not need an explicit Float → α cast helper.

@[reducible, inline]

abbrev TorchLean.ModelZoo.selectsCompiledBackend : List String → Bool

Detect --backend compiled in either --backend=compiled or split-flag form.

@[reducible, inline]

abbrev TorchLean.ModelZoo.forceGpuArgs (exeName : String) (args : List String) : Except String (List String)

Reject --cpu and add CUDA/runtime flags expected by GPU-first commands.

This helper only rewrites command-line intent before the standard runtime parser runs. It does not change the lower-level runtime semantics.

@[reducible, inline]

abbrev TorchLean.ModelZoo.requireEagerBackend (exeName : String) (args : List String) : Except String Unit

Reject the proof-compiled backend for commands that require eager runtime execution.

@[reducible, inline]

abbrev TorchLean.ModelZoo.forceGpuEagerArgs (exeName : String) (args : List String) : Except String (List String)

Reject compiled backend and force the CUDA-first flags expected by eager GPU examples.

@[reducible, inline]

abbrev TorchLean.ModelZoo.runForcedFloat (exeName : String) (args : List String) (normalize : List String → Except String (List String)) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) : IO UInt32

Run a Float-only command after normalizing its runtime flags.

GPU-first examples use this to keep the public Runtime.runFloat path while inserting required CUDA/eager flags before the standard parser runs.

@[reducible, inline]

abbrev TorchLean.ModelZoo.runGpuFloat (exeName : String) (args : List String) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) : IO UInt32

Run a Float-only command after forcing CUDA runtime flags.

@[reducible, inline]

abbrev TorchLean.ModelZoo.runGpuEagerFloat (exeName : String) (args : List String) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) : IO UInt32

Run a Float-only command after forcing CUDA eager-runtime flags.

def TorchLean.ModelZoo.deviceName (opts : Options) : String

Runtime device label used by public example banners and notes.

def TorchLean.ModelZoo.deviceNote (opts : Options) : String

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

def TorchLean.ModelZoo.bannerWithDevice (exeName desc : String) (opts : Options) : String

Standard model-zoo banner shape: executable name, short description, and selected device.

def TorchLean.ModelZoo.bannerWithDeviceDetails (exeName desc details : String) (opts : Options) : String

Standard two-line model-zoo banner: headline plus one indented detail/note line, both carrying the selected device on the headline.

@[reducible, inline]

abbrev TorchLean.ModelZoo.effectiveCudaMemWatch (opts : Runtime.Autograd.Torch.Options) (steps requested : ℕ) : ℕ

Choose a CUDA memory-watch cadence for public examples.

Users can pass --cuda-mem-watch N to choose an exact cadence. When no cadence is supplied, long CUDA runs sample about ten times over the requested training horizon. Short runs and CPU runs stay quiet by default, so the examples do not print allocator telemetry unless it is likely to be useful.

@[reducible, inline]

abbrev TorchLean.ModelZoo.cudaMemWatchNote (opts : Runtime.Autograd.Torch.Options) (steps requested : ℕ) : String

Standard TrainLog note for the effective CUDA memory-watch cadence.

@[reducible, inline]

abbrev TorchLean.ModelZoo.reportCudaMemWatch (opts : Runtime.Autograd.Torch.Options) (watchEvery totalSteps done : ℕ) (state? : Option NN.API.Common.CudaMemWatchState) : IO (Option NN.API.Common.CudaMemWatchState)

Maybe print a one-line CUDA allocator report.

The report samples the native allocator at a fixed cadence and warns if the observed free-memory slope would cross zero before the requested training horizon.

@[reducible, inline]

abbrev TorchLean.ModelZoo.shouldLogStep (logEvery done : ℕ) : Bool

Return whether a completed training step should emit a progress report.

The convention is shared across example trainers: logEvery = 0 disables progress output; otherwise we log at exact multiples of the completed-step count.

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

Fail with a tagged userError if a boolean condition is false.

Executable workflows use this for named precondition checks such as Common.check exeName "loss finite" (loss == loss).

def TorchLean.ModelZoo.writeBeforeAfterLossLogPath (path : System.FilePath) (title : String) (steps : ℕ) (loss0 loss1 : Float) (notes : Array String := #[]) : IO Unit

Write a standard JSON training artifact for routines that record an initial and final loss.

The function uses Runtime.Training.TrainLog.beforeAfterLoss and the stable TrainLog JSON format. The output schema is independent of the model, dataset, and runtime backend.

def TorchLean.ModelZoo.writeBeforeAfterLossLog (dest : Training.LogDestination) (title : String) (steps : ℕ) (loss0 loss1 : Float) (notes : Array String := #[]) : IO Unit

Write a before/after loss log to an explicit logging destination.

LogDestination.disabled is a no-op, mirroring wandb disabled for runs where metrics should stay on stdout only.

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

Write a one-series scalar curve to an explicit logging destination.

def TorchLean.ModelZoo.writeCurveTrainLog (dest : Training.LogDestination) (title : String) (curve : 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 owns a Training.Curve and wants the richer TrainLog artifact shape rather than the default "loss" curve writer.

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

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

Use this when a command accumulates a Training.MetricHistory with explicit series names/colors and then want to publish the richer TrainLog form without rebuilding the same toTrainLog + writeTrainLog boundary in every example file.

def TorchLean.ModelZoo.writeTrainLogPath (path : System.FilePath) (log : Training.TrainLog) : IO Unit

Write a prepared TrainLog JSON artifact and report the file path.

def TorchLean.ModelZoo.writeTrainLog (dest : Training.LogDestination) (log : Training.TrainLog) : IO Unit

Write a prepared TrainLog to a destination that may be disabled.

@[reducible, inline]

abbrev TorchLean.ModelZoo.printCurveLossSummary (steps : ℕ) (curve : Runtime.Training.Curve) : IO Unit

Print the standard first/last loss summary for a scalar training curve.

def TorchLean.ModelZoo.trainFixedCurveFloat {σ τ : Shape} (mkModel : ModelBuilder (SequentialModel σ τ)) (mkModuleDef : (model : SequentialModel σ τ) → ScalarModuleDef (modelParamShapes model) [σ, τ]) (mkOptim : (paramShapes : List Shape) → Runtime.Autograd.TorchLean.Optimizer Float paramShapes) (opts : Options) (sample : SupervisedSample Float σ τ) (steps : ℕ) (cudaMemWatch : ℕ := 0) : IO Training.Curve

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