Shared Real-Data Helpers for Model Examples

The model examples should exercise real data paths. We keep the shared pieces here:

• loading a prepared CIFAR-10 NPY minibatch,
• reading a local text corpus, and
• printing the same "how to prepare data" hint everywhere.

The data files are prepared by scripts/datasets/download_example_data.py; examples report missing inputs explicitly instead of silently falling back to synthetic tensors.

def NN.Examples.Models.RealData.cifarChannels : ℕ

Number of channels in the prepared CIFAR-10 image tensors.

def NN.Examples.Models.RealData.cifarHeight : ℕ

Height of the prepared CIFAR-10 image tensors.

def NN.Examples.Models.RealData.cifarWidth : ℕ

Width of the prepared CIFAR-10 image tensors.

def NN.Examples.Models.RealData.cifarClasses : ℕ

Number of CIFAR-10 classes, hence the width of one-hot targets.

def NN.Examples.Models.RealData.defaultCifarRows : ℕ

Default row budget for CIFAR-10 model-zoo commands.

def NN.Examples.Models.RealData.imagenet64Channels : ℕ

Number of channels in converted ImageNet-style image tensors.

def NN.Examples.Models.RealData.imagenet64Height : ℕ

Height of converted ImageNet-style image tensors.

def NN.Examples.Models.RealData.imagenet64Width : ℕ

Width of converted ImageNet-style image tensors.

def NN.Examples.Models.RealData.imagenet64Classes : ℕ

Number of ImageNet-style classes expected by the converted label path.

def NN.Examples.Models.RealData.defaultImageNet64Rows : ℕ

Default row budget for ImageNet64 model-zoo runs.

instance NN.Examples.Models.RealData.instNeZeroNatCifarChannels : NeZero cifarChannels

instance NN.Examples.Models.RealData.instNeZeroNatCifarHeight : NeZero cifarHeight

instance NN.Examples.Models.RealData.instNeZeroNatCifarWidth : NeZero cifarWidth

instance NN.Examples.Models.RealData.instNeZeroNatCifarClasses : NeZero cifarClasses

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Channels : NeZero imagenet64Channels

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Height : NeZero imagenet64Height

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Width : NeZero imagenet64Width

instance NN.Examples.Models.RealData.instNeZeroNatImagenet64Classes : NeZero imagenet64Classes

@[reducible, inline]

abbrev NN.Examples.Models.RealData.CifarImage : Shape

Shape of one CIFAR-10 image after conversion to CHW layout.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.CifarTarget : Shape

One-hot CIFAR-10 target shape.

def NN.Examples.Models.RealData.cropCifarImages (batch h w : ℕ) (hH : h ≤ cifarHeight) (hW : w ≤ cifarWidth) (x : TorchLean.Tensor.T Float (TorchLean.Shape.images batch cifarChannels cifarHeight cifarWidth)) : TorchLean.Tensor.T Float (TorchLean.Shape.images batch cifarChannels h w)

Take the top-left h × w view of a CIFAR image batch.

def NN.Examples.Models.RealData.cropCifarBatch (batch h w : ℕ) (hH : h ≤ cifarHeight) (hW : w ≤ cifarWidth) (sample : TorchLean.Sample.Batch Float batch CifarImage CifarTarget) : TorchLean.SupervisedSample Float (TorchLean.Shape.images batch cifarChannels h w) (TorchLean.Shape.mat batch cifarClasses)

Crop a CIFAR minibatch while leaving the one-hot class labels unchanged.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.ImageNet64Image : Shape

ImageNet-style converted image shape used by the higher-resolution diffusion example.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.ImageNet64Target : Shape

One-hot target shape for ImageNet-style folders.

The diffusion example ignores labels, but reusing Data.LabeledSource keeps the data path identical to the supervised examples and lets class-directory conversion catch malformed labels early.

def NN.Examples.Models.RealData.missingCifarHint : String

Error message shown when a CIFAR-backed example cannot find the prepared arrays.

def NN.Examples.Models.RealData.missingImageNet64Hint : String

Error message shown when an ImageNet64-backed example cannot find the prepared arrays.

def NN.Examples.Models.RealData.missingTextHint : String

Error message shown when a text-model example cannot find a corpus.

def NN.Examples.Models.RealData.missingAutoMpgHint : String

Error message shown when the Auto MPG CSV is missing.

def NN.Examples.Models.RealData.missingHouseholdPowerHint : String

Error message shown when the household-power forecasting dataset is missing.

def NN.Examples.Models.RealData.tinyShakespearePath : System.FilePath

Default local path for the Tiny Shakespeare corpus.

def NN.Examples.Models.RealData.tinyStoriesValidPath : System.FilePath

Default local path for the TinyStories validation split.

def NN.Examples.Models.RealData.missingTinyShakespeareHint : String

Data-preparation hint for commands that only need Tiny Shakespeare.

def NN.Examples.Models.RealData.missingTinyShakespeareOrTinyStoriesHint : String

Data-preparation hint for commands that accept both Tiny Shakespeare and TinyStories.

def NN.Examples.Models.RealData.NpyDatasets.parseCifar (args : List String) : Except String (TorchLean.ModelZoo.NpyDataFlags × List String)

def NN.Examples.Models.RealData.NpyDatasets.parseImageNet64 (args : List String) : Except String (TorchLean.ModelZoo.NpyDataFlags × List String)

Parse the shared flags for an ImageNet-style 64x64 NPY dataset.

The expected input is produced by scripts/datasets/torchlean_data_convert.py image-folder; that converter handles JPEG/PNG decoding, RGB conversion, resizing, class-directory labels, and the final NCHW layout. Lean then reads only the simple .npy tensors.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.CifarLoggedTrainFlags : Type

Parsed CIFAR dataset and fixed-sample training flags for runnable model examples.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.CifarModelTrainFlags : Type

Parsed CIFAR dataset and optimizer/training flags for classifier examples.

def NN.Examples.Models.RealData.CifarLoggedTrainFlags.parse (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 10) : Except String CifarLoggedTrainFlags

Parse the standard CIFAR plus fixed-step training flags and reject unused arguments.

Generative examples use the same prepared CIFAR arrays and the same loss-curve logging contract; only the model and target construction differ.

def NN.Examples.Models.RealData.CifarModelTrainFlags.parse (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 1) (defaultLr : Float := 1e-3) : Except String (CifarModelTrainFlags × List String)

Parse the standard CIFAR plus optimizer/training flags.

Vision examples share the same CIFAR data boundary and optimizer controls; architecture files only need to provide the model constructor and logging title. Any remaining arguments are preserved so the caller can forward runtime flags such as --cpu, --cuda, or --backend compiled to the public Trainer.RunConfig parser.

def NN.Examples.Models.RealData.cifarTrainNotes (opts : TorchLean.Options) (flags : CifarLoggedTrainFlags) (extra : Array String := #[]) : Array String

Common TrainLog notes for CIFAR-backed examples.

def NN.Examples.Models.RealData.ForecastWindowDataFlags.parse (exeName : String) (args : List String) (defaultWindows : ℕ := 512) (defaultReportOffset : ℕ := 96) : Except String (TorchLean.ModelZoo.ForecastWindowDataFlags × List String)

Parse the shared flags for household-power forecasting windows.

Forecasting commands share --data-dir, --x, --y, --windows, --report-offset, and --seed.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.HouseholdPowerModelTrainFlags : Type

Parsed household-power forecasting data plus optimizer/training flags.

def NN.Examples.Models.RealData.HouseholdPowerModelTrainFlags.parse (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 100) (defaultLr : Float := 1e-2) (defaultWindows : ℕ := 512) (defaultReportOffset : ℕ := 96) : Except String (HouseholdPowerModelTrainFlags × List String)

Parse the standard household-power forecasting flags plus optimizer/training flags.

The forecasting command still owns the model and reporting logic, but the shared data/runtime flag surface lives here with the other real-data code.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.requireSupervisedNpyFiles (exeName xLabel : String) (xPath : System.FilePath) (yLabel : String) (yPath : System.FilePath) (hint : String) : IO Unit

Require that a paired supervised .npy dataset exists before training starts.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.requireCsvFile (exeName : String) (csvPath : System.FilePath) (hint : String) : IO Unit

Require that a CSV path exists before a tabular regression command starts training.

def NN.Examples.Models.RealData.loadCifarLoader (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (API.Data.BatchLoader Float batch CifarImage CifarTarget)

def NN.Examples.Models.RealData.cifarDataset (nRows : ℕ) (xPath yPath : System.FilePath) : TorchLean.Trainer.Dataset CifarImage CifarTarget

Public trainer dataset for prepared CIFAR-10 NPY image/label arrays.

def NN.Examples.Models.RealData.cifarClassifierNotes (batch : ℕ) (flags : CifarModelTrainFlags) (extra : Array String := #[]) : Array String

Common training-log notes for CIFAR-backed classifier examples.

def NN.Examples.Models.RealData.cifarCurve (exeName : String) (args : List String) (defaultLogPath : System.FilePath) (defaultSteps : ℕ := 10) (banner : TorchLean.Options → String) (seriesName title : String) (extraNotes : TorchLean.Options → CifarLoggedTrainFlags → Array String := fun (x : TorchLean.Options) (x_1 : CifarLoggedTrainFlags) => #[]) (train : TorchLean.Options → CifarLoggedTrainFlags → IO TorchLean.Training.Curve) : IO UInt32

Shared main entrypoint for CIFAR-backed curve-reporting commands.

Some commands do not match the public trainer result shape because they manage several modules or log one custom scalar curve instead of a single trainer report. They still share the same CIFAR parsing, runtime parsing, CUDA-memory notes, and TrainLog boundary.

def NN.Examples.Models.RealData.loadCifarBatches (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (List (TorchLean.Sample.Batch Float batch CifarImage CifarTarget))

Load one shuffled epoch of full CIFAR-10 minibatches from prepared .npy arrays.

def NN.Examples.Models.RealData.loadCifarBatch (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (TorchLean.Sample.Batch Float batch CifarImage CifarTarget)

Load the first full CIFAR-10 minibatch from the shared CIFAR loader.

def NN.Examples.Models.RealData.loadImageNet64Loader (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (API.Data.BatchLoader Float batch ImageNet64Image ImageNet64Target)

Load a user-prepared ImageNet-style 64x64 minibatch.

This loader reads prepared .npy arrays rather than JPEG files. The Python converter is the trust boundary for filesystem image decoding and resizing; this Lean path checks the resulting tensor shape and class range before handing the batch to examples.

def NN.Examples.Models.RealData.loadImageNet64Batches (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (List (TorchLean.Sample.Batch Float batch ImageNet64Image ImageNet64Target))

Load one shuffled epoch of full ImageNet64-style minibatches from prepared .npy arrays.

def NN.Examples.Models.RealData.loadImageNet64Batch (exeName : String) (batch nRows seed : ℕ) (xPath yPath : System.FilePath) : IO (TorchLean.Sample.Batch Float batch ImageNet64Image ImageNet64Target)

Load the first full ImageNet64-style minibatch from the shared ImageNet64 loader.

def NN.Examples.Models.RealData.loadCifarVectorBatch (cfg : TorchLean.nn.models.VectorGenerativeConfig) (hData : cfg.dataDim ≤ Shape.size CifarImage) (exeName : String) (xPath yPath : System.FilePath) (nRows seed : ℕ) : IO (TorchLean.Tensor.T Float (TorchLean.nn.models.vectorDataShape cfg))

Load a CIFAR minibatch and expose it as a compact flattened vector batch.

The file paths and download hints remain in NN.Examples, while the flattening logic lives in the public generative-model API so users can reuse it with their own image tensors.

def NN.Examples.Models.RealData.cifarVectorDataset {τ : Shape} (cfg : TorchLean.nn.models.VectorGenerativeConfig) (hData : cfg.dataDim ≤ Shape.size CifarImage) (exeName : String) (mkSample : TorchLean.Tensor.T Float (TorchLean.nn.models.vectorDataShape cfg) → TorchLean.SupervisedSample Float (TorchLean.nn.models.vectorDataShape cfg) τ) (xPath yPath : System.FilePath) (nRows seed : ℕ) : TorchLean.Trainer.Dataset (TorchLean.nn.models.vectorDataShape cfg) τ

Public singleton dataset for compact vector generative examples over flattened CIFAR batches.

Autoencoder, VAE, and VQ-VAE examples all load one real CIFAR batch, flatten it to the compact vector boundary, build one supervised sample, and hand that sample to the public trainer API. The sample itself may be Float-specific; this dataset constructor casts it into the runtime-selected scalar so the command still works across the ordinary public runtime backends.

@[reducible, inline]

abbrev NN.Examples.Models.RealData.TextCorpusFlags : Type

Shared text-corpus CLI/data boundary for local text-model examples.

def NN.Examples.Models.RealData.TextCorpusFlags.parse (args : List String) : Except String (TextCorpusFlags × List String)

Parse the shared --data-file flag used by local text-model examples.

--tiny-shakespeare is accepted as an explicit shortcut for the default corpus path.

def NN.Examples.Models.RealData.TextCorpusFlags.read (exeName : String) (flags : TextCorpusFlags) : IO String

Read the selected text corpus and fail with a shared preparation hint when it is missing.