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 example 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 example 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 : Spec.Shape

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

@[reducible, inline]

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

One-hot CIFAR-10 target shape.

def NN.Examples.Models.RealData.Internal.cropCifarImages (batchSize cropHeight cropWidth : ℕ) (heightFits : cropHeight ≤ cifarHeight) (widthFits : cropWidth ≤ cifarWidth) (x : TorchLean.Tensor Float [batchSize, cifarChannels, cifarHeight, cifarWidth]) : TorchLean.Tensor Float [batchSize, cifarChannels, cropHeight, cropWidth]

Take the top-left cropHeight × cropWidth view of a CIFAR image batch.

def NN.Examples.Models.RealData.cropCifarImages (batchSize cropHeight cropWidth : ℕ) (x : TorchLean.Tensor Float [batchSize, cifarChannels, cifarHeight, cifarWidth]) : Except String (TorchLean.Tensor Float [batchSize, cifarChannels, cropHeight, cropWidth])

Take the top-left cropHeight × cropWidth view of a CIFAR image batch.

Invalid crop sizes are reported at the executable boundary.

def NN.Examples.Models.RealData.cropCifarBatch (batchSize cropHeight cropWidth : ℕ) (sample : TorchLean.Sample.Batch Float batchSize CifarImage CifarTarget) : Except String (TorchLean.Sample.Supervised Float [batchSize, cifarChannels, cropHeight, cropWidth] [batchSize, cifarClasses])

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

@[reducible, inline]

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

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

@[reducible, inline]

abbrev NN.Examples.Models.RealData.ImageNet64Target : Spec.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.NpyDatasets.parseCifar (args : List String) : Except String (Support.NpyDataFlags × List String)

Parse the shared NPY data flags with CIFAR-10's default paths and row count filled in.

def NN.Examples.Models.RealData.NpyDatasets.parseImageNet64 (args : List String) : Except String (Support.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) (defaultLearningRate : 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 --device cpu, --device cuda, or --execution typed-graph to the public Trainer.RunConfig parser.

def NN.Examples.Models.RealData.ForecastWindowDataFlags.parse (exeName : String) (args : List String) (defaultWindows : ℕ := 512) (defaultReportOffset : ℕ := 96) : Except String (Support.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) (defaultLearningRate : 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.

def NN.Examples.Models.RealData.loadCifarLoader (exeName : String) (batchSize rowCount seed : ℕ) (xPath yPath : System.FilePath) : IO (TorchLean.Data.Loader Float batchSize CifarImage CifarTarget)

Build a batched CIFAR-10 loader from the image and label .npy files.

Both files are required up front, with a hint pointing at the converter script, so a missing dataset fails with something actionable rather than a decode error halfway through the first epoch.

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

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

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

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

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

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

def NN.Examples.Models.RealData.loadImageNet64Loader (exeName : String) (batchSize rowCount seed : ℕ) (xPath yPath : System.FilePath) : IO (TorchLean.Data.Loader Float batchSize 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) (batchSize rowCount seed : ℕ) (xPath yPath : System.FilePath) : IO (Array (TorchLean.Sample.Batch Float batchSize ImageNet64Image ImageNet64Target))

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

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

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

def NN.Examples.Models.RealData.loadCifarFeatureBatch (batchSize : ℕ) (config : TorchLean.nn.models.Generative.Config) (exeName : String) (xPath yPath : System.FilePath) (rowCount seed : ℕ) : IO (TorchLean.Tensor Float (config.dataShape [batchSize]))

Load a CIFAR minibatch, flatten each channel-first image, and retain its first config.dataWidth values. This is a prefix of the image buffer, not a spatial resize or learned feature extraction. Widths larger than the full image are rejected.

def NN.Examples.Models.RealData.cifarFeatureDataset {τ : Spec.Shape} (batchSize : ℕ) (config : TorchLean.nn.models.Generative.Config) (exeName : String) (sampleOfFeatures : TorchLean.Tensor Float (config.dataShape [batchSize]) → TorchLean.Sample.Supervised Float (config.dataShape [batchSize]) τ) (xPath yPath : System.FilePath) (rowCount seed : ℕ) : TorchLean.Trainer.Dataset (config.dataShape [batchSize]) τ

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

Autoencoder and supervised latent-bottleneck examples 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 arithmetic representation 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.help : Array String

Command-line options shared by local text-corpus 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.

structure NN.Examples.Models.RealData.TextWindowFlags : Type

Text corpus selection plus the number of causal training windows to expose.

• corpus : TextCorpusFlags

  Selected UTF-8 corpus.

• windows : ℕ

  Number of approximately evenly spaced windows in the finite training dataset.

@[instance_reducible]

instance NN.Examples.Models.RealData.instReprTextWindowFlags : Repr TextWindowFlags

def NN.Examples.Models.RealData.instReprTextWindowFlags.repr : TextWindowFlags → ℕ → Std.Format

def NN.Examples.Models.RealData.TextWindowFlags.help (defaultWindows : ℕ) : Array String

Command-line options shared by finite-window text examples.

def NN.Examples.Models.RealData.TextWindowFlags.parse (exeName : String) (defaultWindows : ℕ) (args : List String) : Except String (TextWindowFlags × List String)

Parse a text corpus and a positive --windows count.

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

Read the selected text corpus.