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.Npy.Options × 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.Npy.Options × 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.

def NN.Examples.Models.RealData.Forecast.Options.parse (exeName : String) (args : List String) (defaultWindows : ℕ := 512) (defaultReportOffset : ℕ := 96) : Except String (Support.Forecast.Options × List String)

Parse the shared flags for household-power forecasting windows.

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

def NN.Examples.Models.RealData.Internal.loadImageLoader (imageShape : Spec.Shape) (classes : ℕ) (datasetName missingHint recoveryHint exeName : String) (batchSize rowCount seed : ℕ) (xPath yPath : System.FilePath) : IO (TorchLean.Data.Loader Float batchSize imageShape [classes])

Load prepared labeled images with dataset-specific preparation and recovery hints.

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.trainingNotes (dataset : String) (batchSize : ℕ) (flags : Support.Training.Options Support.Npy.Options) (extra : Array String := #[]) : Array String

Dataset and optimizer metadata for training on prepared NPY tensors.

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.trainCifarClassifier (batchSize cropHeight cropWidth : ℕ) (exeName logTitle : String) (model : TorchLean.nn.Builder (TorchLean.nn.Sequential [batchSize, cifarChannels, cropHeight, cropWidth] [batchSize, cifarClasses])) (runtime : TorchLean.Runtime.Config) (flags : Support.Training.Options Support.Npy.Options) (extraNotes : Array String := #[]) : IO TorchLean.Trainer.Report

Train a cropped CIFAR classifier with the examples' shared Adam and cross-entropy policy.

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.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.

def NN.Examples.Models.RealData.Corpus.help : Array String

Command-line options shared by local text-corpus examples.

def NN.Examples.Models.RealData.Corpus.parse (args : List String) : Except String (System.FilePath × 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.Corpus.read (exeName : String) (path : System.FilePath) : IO String

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

structure NN.Examples.Models.RealData.Corpus.Options : Type

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

• corpus : System.FilePath

  Selected UTF-8 corpus.

• windows : ℕ

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

@[instance_reducible]

instance NN.Examples.Models.RealData.Corpus.instReprOptions : Repr Options

def NN.Examples.Models.RealData.Corpus.instReprOptions.repr : Options → ℕ → Std.Format

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

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

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

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

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

Read the selected text corpus.