NN.API.Common

Shared helpers used across TorchLean workflows and entrypoints: typed tensor constructors, casting between scalar backends, and shared Except/IO utilities.

Common Helpers For Workflows And Entry Points

This module contains helper functions that show up repeatedly in executable workflows.

What belongs here:

• casting Spec.Tensor Float into an arbitrary scalar backend α (given Float → α)
• building typed tensors from raw lists (tensorF, vecF, matF)
• bridging Except String into IO (orThrow)
• running model commands under a chosen scalar backend via --dtype (see NN.API.DType)

What does not belong here:

• core semantics/proofs (those live under NN / NN.Proofs)
• command-specific CLI parsing that belongs with a model or tool entrypoint

PyTorch Mapping Notes

If you're coming from PyTorch, this module plays the role of the shared utility layer often written around:

• torch.tensor([...], dtype=..., device=...)
• choosing a dtype/backend based on CLI flags
• dataset loading and runnable workflow code

The main difference is that TorchLean tracks shapes in types, so tensor constructors here return Except String ... rather than silently reshaping.

def NN.API.Common.castTensor {α : Type} (cast : Float → α) {s : Spec.Shape} (t : Spec.Tensor Float s) : Spec.Tensor α s

Cast a tensor elementwise while preserving its type-level shape.

def NN.API.Common.orThrow {α : Type} (tag : String := "Example") : 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.

def NN.API.Common.modelZooTrainLog (stem : String) : System.FilePath

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

def NN.API.Common.check (tag 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 NN.API.Common.requirePositiveNatFlag (exeName flag : String) (value : ℕ) : Except String Unit

Validate that a natural-number CLI flag is positive.

def NN.API.Common.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 NN.API.Common.writeTrainLog (path : System.FilePath) (log : Runtime.Training.TrainLog) : IO Unit

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

def NN.API.Common.writeTrainLogTo (dest : Runtime.Training.LogDestination) (log : Runtime.Training.TrainLog) : IO Unit

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

def NN.API.Common.writeBeforeAfterLossLog (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 NN.API.Common.writeBeforeAfterLossLogTo (dest : Runtime.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 NN.API.Common.printTrainReport {α : Type} [ToString α] (steps : ℕ) (report : TorchLean.Trainer.TrainReport α) : IO Unit

Print the standard before/after loss summary returned by fit helpers.

structure NN.API.Common.CurveEndpoints : Type

First and last point of a scalar training curve, ready for summaries.

• finalStep : ℕ

  Step used for the final point.

• first : Float

  First recorded metric value.

• last : Float

  Last recorded metric value.

def NN.API.Common.instReprCurveEndpoints.repr : CurveEndpoints → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprCurveEndpoints : Repr CurveEndpoints

def NN.API.Common.curveEndpoints? (curve : Runtime.Training.Curve) : Option CurveEndpoints

Read the first and last values from a scalar curve.

If curve.steps is empty, the final step falls back to the last value index. Empty value arrays are reported as errors instead of printing a fake 0.0 summary.

def NN.API.Common.requireCurveEndpoints (context : String) (curve : Runtime.Training.Curve) : IO CurveEndpoints

Require first/last scalar values from a training curve, or raise a user-facing error.

def NN.API.Common.printCurveLossSummary (steps : ℕ) (curve : Runtime.Training.Curve) : IO Unit

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

def NN.API.Common.writeCurveLog (path : System.FilePath) (title : String) (curve : Runtime.Training.Curve) (seriesName : String := "loss") (notes : Array String := #[]) : IO Unit

Write a one-series scalar curve as a standard TrainLog JSON artifact.

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

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

structure NN.API.Common.LoggedTrainFlags : Type

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

• steps : ℕ

  Number of optimizer updates.

• batchSize : ℕ

  Number of samples consumed by one public in-memory training step.

• log : Runtime.Training.LogDestination

  Logging destination. Use --log false / off / none to disable.

• logPath : System.FilePath

  Path where the JSON TrainLog should be written.

• cudaMemWatch : ℕ

  CUDA allocator telemetry cadence shared by fixed-sample and custom training loops.

@[implicit_reducible]

instance NN.API.Common.instReprLoggedTrainFlags : Repr LoggedTrainFlags

def NN.API.Common.instReprLoggedTrainFlags.repr : LoggedTrainFlags → ℕ → Std.Format

def NN.API.Common.parseLoggedTrainFlags (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (allowZeroSteps : Bool := false) : Except String (LoggedTrainFlags × List String)

Parse common training flags: positive --steps, positive optional --batch-size, plus optional --log.

--log <path> writes the standard local JSON artifact. --log false, --log off, or --log none disables artifact writing while preserving the parsed step count.

structure NN.API.Common.ModelTrainFlagsextends NN.API.Common.LoggedTrainFlags : 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.

• steps : ℕ
• batchSize : ℕ
• log : Runtime.Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float

  Learning rate for the default Adam optimizer used by examples.

@[implicit_reducible]

instance NN.API.Common.instReprModelTrainFlags : Repr ModelTrainFlags

def NN.API.Common.instReprModelTrainFlags.repr : ModelTrainFlags → ℕ → Std.Format

def NN.API.Common.parseModelTrainFlags (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) (allowZeroSteps : Bool := false) : Except String (ModelTrainFlags × List String)

Parse the standard model-training flags: --steps, --log, --lr, and CUDA telemetry.

structure NN.API.Common.SeededModelTrainFlagsextends NN.API.Common.ModelTrainFlags : 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.

• steps : ℕ
• batchSize : ℕ
• log : Runtime.Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• seed : ℕ

  Seed used for model initialization, synthetic data, or row order.

def NN.API.Common.instReprSeededModelTrainFlags.repr : SeededModelTrainFlags → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprSeededModelTrainFlags : Repr SeededModelTrainFlags

def NN.API.Common.parseSeededModelTrainFlags (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) (allowZeroSteps : Bool := false) : Except String (SeededModelTrainFlags × List String)

Parse the standard model-training flags together with --seed.

Examples use this when model initialization, synthetic data, or row order needs a reproducible seed.

Progress Cadence Helpers

def NN.API.Common.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.

CUDA Memory Watch Helpers

def NN.API.Common.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.

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

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

structure NN.API.Common.CudaMemWatchState : Type

State for a simple CUDA-memory drift detector.

The first reported sample becomes the baseline. Later samples compare current CUDA free memory against that baseline and warn once if the observed per-step drop projects failure before the requested run length.

• firstStep : ℕ
• firstFreeBytes : ℕ
• warned : Bool

def NN.API.Common.instReprCudaMemWatchState.repr : CudaMemWatchState → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprCudaMemWatchState : Repr CudaMemWatchState

def NN.API.Common.reportCudaMemWatch (opts : Runtime.Autograd.Torch.Options) (watchEvery totalSteps done : ℕ) (state? : Option CudaMemWatchState) : IO (Option 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.

def NN.API.Common.adamOptimizer {α : Type} [Semantics.Scalar α] [Runtime.Scalar α] (cast : Float → α) (ps : List Shape) (lr : Float) : Runtime.Autograd.TorchLean.Optimizer α ps

Default Adam optimizer constructor used by supervised and vision examples.

The reusable part is the optimizer convention, not the model. Individual examples still own their architecture and loss, while this helper keeps the Adam hyperparameter spelling identical across MLP, CNN, ResNet, ViT, and similar model commands.

def NN.API.Common.runAnyOrFloat (exeName : String) (args : List String) (preferFloat : List String → Bool) (banner : Runtime.Autograd.Torch.Options → String) (anyK : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → (Float → α) → Runtime.Autograd.Torch.Options → List String → IO Unit) (floatK : Runtime.Autograd.Torch.Options → List String → IO Unit) (printOk : Bool := true) : 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.

def NN.API.Common.runAnyOrFloatNoCast (exeName : String) (args : List String) (preferFloat : List String → Bool) (banner : Runtime.Autograd.Torch.Options → String) (anyK : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → Runtime.Autograd.Torch.Options → List String → IO Unit) (floatK : Runtime.Autograd.Torch.Options → List String → IO Unit) (printOk : Bool := true) : 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.

def NN.API.Common.runFloat (exeName : String) (args : List String) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) (printOk : Bool := true) : 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.

Runtime-flag normalization

def NN.API.Common.selectsCompiledBackend : List String → Bool

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

def NN.API.Common.forceGpuArgs (exeName : String) (args : List String) (extraFlags : List String := ["--fast-kernels"]) : 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.

def NN.API.Common.requireEagerBackend (exeName : String) (args : List String) : Except String Unit

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

def NN.API.Common.forceGpuEagerArgs (exeName : String) (args : List String) (extraFlags : List String := ["--fast-kernels"]) : Except String (List String)

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

def NN.API.Common.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) (printOk : Bool := true) : 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.

def NN.API.Common.runGpuFloat (exeName : String) (args : List String) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) (extraFlags : List String := ["--fast-kernels"]) (printOk : Bool := true) : IO UInt32

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

def NN.API.Common.runGpuEagerFloat (exeName : String) (args : List String) (banner : Runtime.Autograd.Torch.Options → String) (k : Runtime.Autograd.Torch.Options → List String → IO Unit) (extraFlags : List String := ["--fast-kernels"]) (printOk : Bool := true) : IO UInt32

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

Common model-run parsers

structure NN.API.Common.WindowOptions : Type

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

• windows : ℕ

  Number of windows used by the training set, sampler, or cyclic schedule.

@[implicit_reducible]

instance NN.API.Common.instReprWindowOptions : Repr WindowOptions

def NN.API.Common.instReprWindowOptions.repr : WindowOptions → ℕ → Std.Format

def NN.API.Common.WindowOptions.parse (exeName : String) (args : List String) (defaultWindows : ℕ) : Except String (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.

structure NN.API.Common.CheckpointOptions : Type

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

• loadParams? : Option System.FilePath

  Optional checkpoint path loaded before training/generation.

• saveParams? : Option System.FilePath

  Optional checkpoint path written after training.

@[implicit_reducible]

instance NN.API.Common.instReprCheckpointOptions : Repr CheckpointOptions

def NN.API.Common.instReprCheckpointOptions.repr : CheckpointOptions → ℕ → Std.Format

def NN.API.Common.CheckpointOptions.parse (args : List String) : Except String (CheckpointOptions × List String)

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

structure NN.API.Common.DiffusionScheduleFlags : Type

Diffusion schedule knobs shared by model-zoo diffusion commands.

• T : ℕ

  Number of diffusion timesteps in the schedule.

• betaStart : Float

  First beta value in the schedule.

• betaEnd : Float

  Final beta value in the schedule.

def NN.API.Common.instReprDiffusionScheduleFlags.repr : DiffusionScheduleFlags → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprDiffusionScheduleFlags : Repr DiffusionScheduleFlags

def NN.API.Common.DiffusionScheduleFlags.parse (args : List String) (defaultT : ℕ := 100) (defaultBetaStart : Float := 1e-4) (defaultBetaEnd : Float := 0.12) : Except String (DiffusionScheduleFlags × List String)

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

def NN.API.Common.DiffusionScheduleFlags.trainLogNotes (cfg : DiffusionScheduleFlags) : Array String

Standard TrainLog metadata for a diffusion schedule.

structure NN.API.Common.ImageArtifactFlags : Type

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

• reconstructStep? : Option ℕ

  Optional timestep used for reconstruction-from-noise artifacts.

• samplePpm? : Option System.FilePath

  Optional path for an unconditional sample image.

• referencePpm? : Option System.FilePath

  Optional path for the clean reference image.

• noisyPpm? : Option System.FilePath

  Optional path for the noised/intermediate image.

• reconstructPpm? : Option System.FilePath

  Optional path for the reconstructed image.

@[implicit_reducible]

instance NN.API.Common.instReprImageArtifactFlags : Repr ImageArtifactFlags

def NN.API.Common.instReprImageArtifactFlags.repr : ImageArtifactFlags → ℕ → Std.Format

def NN.API.Common.ImageArtifactFlags.parse (args : List String) : Except String (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.

def NN.API.Common.ImageArtifactFlags.trainLogNotes (cfg : ImageArtifactFlags) : Array String

Standard TrainLog metadata for requested image artifacts.

structure NN.API.Common.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.

• trainRows : ℕ

  Number of rows loaded from the prepared training tensors.

• testRows : ℕ

  Number of rows loaded from the prepared held-out tensors.

• evalRows : ℕ

  Prefix length used for deterministic train/test loss reports.

• trainX : System.FilePath

  Training input .npy path.

• trainY : System.FilePath

  Training target .npy path.

• testX : System.FilePath

  Held-out input .npy path.

• testY : System.FilePath

  Held-out target .npy path.

@[implicit_reducible]

instance NN.API.Common.instReprPairedNpyEvalFlags : Repr PairedNpyEvalFlags

def NN.API.Common.instReprPairedNpyEvalFlags.repr : PairedNpyEvalFlags → ℕ → Std.Format

def NN.API.Common.PairedNpyEvalFlags.parse (args : List String) (defaultTrainX defaultTrainY defaultTestX defaultTestY : System.FilePath) (defaultTrainRows defaultTestRows : ℕ) (defaultEvalRows : ℕ := 16) : Except String (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.

def NN.API.Common.PairedNpyEvalFlags.trainLogNotes (cfg : PairedNpyEvalFlags) : Array String

Standard TrainLog metadata for paired train/test NPY tensors.

structure NN.API.Common.CsvArtifactFlags : Type

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

• plotCsv : System.FilePath

  CSV path for the diagnostic artifact.

def NN.API.Common.instReprCsvArtifactFlags.repr : CsvArtifactFlags → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprCsvArtifactFlags : Repr CsvArtifactFlags

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

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

structure NN.API.Common.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.

• xPath : System.FilePath

  Prepared feature/image tensor path.

• yPath : System.FilePath

  Prepared label/target tensor path.

• nRows : ℕ

  Number of rows to read from the prepared arrays.

• seed : ℕ

  Data-loader seed.

@[implicit_reducible]

instance NN.API.Common.instReprNpyDataFlags : Repr NpyDataFlags

def NN.API.Common.instReprNpyDataFlags.repr : NpyDataFlags → ℕ → Std.Format

def NN.API.Common.NpyDataFlags.parse (args : List String) (defaultX defaultY : System.FilePath) (defaultRows : ℕ) : Except String (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.

def NN.API.Common.NpyDataFlags.trainLogNotes (cfg : NpyDataFlags) (datasetName : String) : Array String

Standard TrainLog metadata for an NPY-backed dataset branch.

inductive NN.API.Common.ImageDatasetChoice : Type

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

• imagenet64 : ImageDatasetChoice

  Prepared 64×64 RGB image tensors.

• cifar10 : ImageDatasetChoice

  Prepared CIFAR-10 32×32 RGB tensors.

@[implicit_reducible]

instance NN.API.Common.instReprImageDatasetChoice : Repr ImageDatasetChoice

def NN.API.Common.instReprImageDatasetChoice.repr : ImageDatasetChoice → ℕ → Std.Format

def NN.API.Common.instBEqImageDatasetChoice.beq : ImageDatasetChoice → ImageDatasetChoice → Bool

@[implicit_reducible]

instance NN.API.Common.instBEqImageDatasetChoice : BEq ImageDatasetChoice

def NN.API.Common.ImageDatasetChoice.parse (args : List String) : Except String (ImageDatasetChoice × List String)

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

structure NN.API.Common.ForecastWindowDataFlags : Type

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

• xPath : System.FilePath

  Prepared input-window tensor path.

• yPath : System.FilePath

  Prepared target-window tensor path.

• windows : ℕ

  Number of forecasting windows to use.

• reportOffset : ℕ

  Report window index used for before/after forecast display.

• seed : ℕ

  Data-loader seed.

@[implicit_reducible]

instance NN.API.Common.instReprForecastWindowDataFlags : Repr ForecastWindowDataFlags

def NN.API.Common.instReprForecastWindowDataFlags.repr : ForecastWindowDataFlags → ℕ → Std.Format

def NN.API.Common.ForecastWindowDataFlags.trainLogNotes (cfg : ForecastWindowDataFlags) : Array String

Standard TrainLog metadata for forecasting-window datasets.

structure NN.API.Common.NpyLoggedTrainFlagsextends NN.API.Common.LoggedTrainFlags, NN.API.Common.NpyDataFlags : Type

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

• steps : ℕ
• batchSize : ℕ
• log : Runtime.Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• xPath : System.FilePath
• yPath : System.FilePath
• nRows : ℕ
• seed : ℕ

@[implicit_reducible]

instance NN.API.Common.instReprNpyLoggedTrainFlags : Repr NpyLoggedTrainFlags

def NN.API.Common.instReprNpyLoggedTrainFlags.repr : NpyLoggedTrainFlags → ℕ → Std.Format

def NN.API.Common.parseNpyLoggedTrainFlags (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.

structure NN.API.Common.NpyModelTrainFlagsextends NN.API.Common.ModelTrainFlags, NN.API.Common.NpyDataFlags : Type

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

• steps : ℕ
• batchSize : ℕ
• log : Runtime.Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• xPath : System.FilePath
• yPath : System.FilePath
• nRows : ℕ
• seed : ℕ

@[implicit_reducible]

instance NN.API.Common.instReprNpyModelTrainFlags : Repr NpyModelTrainFlags

def NN.API.Common.instReprNpyModelTrainFlags.repr : NpyModelTrainFlags → ℕ → Std.Format

def NN.API.Common.parseNpyModelTrainFlags (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.

structure NN.API.Common.ForecastWindowModelTrainFlagsextends NN.API.Common.ModelTrainFlags, NN.API.Common.ForecastWindowDataFlags : Type

Common arguments for forecasting-window model-training commands.

• steps : ℕ
• batchSize : ℕ
• log : Runtime.Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• xPath : System.FilePath
• yPath : System.FilePath
• windows : ℕ
• reportOffset : ℕ
• seed : ℕ

@[implicit_reducible]

instance NN.API.Common.instReprForecastWindowModelTrainFlags : Repr ForecastWindowModelTrainFlags

def NN.API.Common.instReprForecastWindowModelTrainFlags.repr : ForecastWindowModelTrainFlags → ℕ → Std.Format

def NN.API.Common.parseForecastWindowModelTrainFlags (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.

structure NN.API.Common.CsvModelTrainFlagsextends NN.API.Common.ModelTrainFlags : Type

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

• steps : ℕ
• batchSize : ℕ
• log : Runtime.Training.LogDestination
• logPath : System.FilePath
• cudaMemWatch : ℕ
• lr : Float
• csvPath : System.FilePath

  CSV file containing model inputs and targets.

• seed : ℕ

  Seed used for model initialization and data shuffling.

def NN.API.Common.instReprCsvModelTrainFlags.repr : CsvModelTrainFlags → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Common.instReprCsvModelTrainFlags : Repr CsvModelTrainFlags

def NN.API.Common.parseCsvModelTrainFlags (exeName : String) (args : List String) (defaultCsv defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) (allowZeroSteps : Bool := false) : Except String (CsvModelTrainFlags × List String)

Parse common flags for a supervised CSV model runner.

Model files choose their default CSV, default log path, step count, and learning rate.

def NN.API.Common.listGen {α : Type} (n : ℕ) (f : ℕ → α) : List α

List generator: [0, 1, ..., n-1] mapped through f.

def NN.API.Common.tensorF {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (xs : List Float) : Except String (Spec.Tensor α (Tensor.shapeOfDims dims))

Build an N-D tensor from a raw list of floats and cast it into the chosen scalar backend.

Fails if xs.length ≠ numel(dims).

def NN.API.Common.tensorFGen {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (f : ℕ → Float) : Except String (Spec.Tensor α (Tensor.shapeOfDims dims))

Generate an N-D tensor by calling f for each element index, then cast into the chosen backend.

The function f is indexed by the flat element index 0..numel-1.

def NN.API.Common.tensorFGen! {α : Type} [Context α] (cast : Float → α) (dims : List ℕ) (f : ℕ → Float) : Spec.Tensor α (Tensor.shapeOfDims dims)

Generate an N-D tensor by calling f for each flat element index, with no failure case.

This is the “total” sibling of tensorFGen: since we generate exactly numel(dims) values, the reshape cannot fail, so we avoid an Except. When you want to build a deterministic constant tensor for an example, this is usually the right tool.

def NN.API.Common.tensorFGenShape! {α : Type} [Context α] (cast : Float → α) (s : Spec.Shape) (f : ℕ → Float) : Spec.Tensor α s

Generate a tensor of a known shape s by calling f for each flat element index, then cast into the chosen backend.

This packages the standard shape-cast pattern used when a tensor is generated from flat indices:

let xDyn : Tensor α (shapeOfDims s.toList) := ...
let x : Tensor α s := by simpa using xDyn

def NN.API.Common.vecF {α : Type} [Context α] (cast : Float → α) (n : ℕ) (xs : List Float) : Except String (Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar))

1D vector tensor constructor specialized to shape Vec n.

Fails if xs.length ≠ n.

def NN.API.Common.vecFGen {α : Type} [Context α] (cast : Float → α) (n : ℕ) (f : ℕ → Float) : Except String (Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar))

Generator variant of vecF.

def NN.API.Common.matF {α : Type} [Context α] (cast : Float → α) (rows cols : ℕ) (xs : List Float) : Except String (Spec.Tensor α (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

2D matrix tensor constructor specialized to shape Mat rows cols.

Fails if xs.length ≠ rows * cols.

def NN.API.Common.matFGen {α : Type} [Context α] (cast : Float → α) (rows cols : ℕ) (f : ℕ → Float) : Except String (Spec.Tensor α (Spec.Shape.dim rows (Spec.Shape.dim cols Spec.Shape.scalar)))

Generator variant of matF.

def NN.API.Common.runWithDType (title : String) (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → (Float → α) → IO Unit) : IO Unit

Run a workflow once under a dtype selected from args (via --dtype / --float32-mode).

This logs the chosen dtype and then calls k with a cast function Float → α for the selected scalar backend.

In particular:

• --dtype=float selects Lean's builtin Float (trusted semantics, executable),
• --dtype=float32 selects TorchLean's verified IEEE32 executable semantics,
• --dtype=complex selects TorchLean's parametric complex scalar over Float32,
• --dtype=real selects ℝ (proof-only; errors at runtime).

def NN.API.Common.runWithRuntimeDType (title : String) (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → IO Unit) : IO Unit

Like runWithDType, but also provides an API.Runtime.Scalar α instance.

Use this when your workflow uses numeric literals (1.0, -3.5, etc.) at runtime.

@[reducible, inline]

abbrev NN.API.Common.mainWithRuntimeDType (title : String) (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → IO Unit) : IO Unit

Entry-point alias for runnable binaries that need runtime float-literal injection.