Simple CNN training example

This is the image-classification companion to the small MLP tutorial. The file shows the public training path in its simplest CNN form: define the layers, choose a trainer, batch the small dataset, and call trainer.train. Shape-indexed tensors and the checked training task remain present, but the first read follows the model code rather than subsystem plumbing.

Check this tutorial module directly:

• lake build NN.Examples.Quickstart.SimpleCnnTrain

For the maintained command-line CNN trainer, use NN/Examples/Models/Vision/Cnn.lean:

• python3 scripts/datasets/download_example_data.py --cifar10
• lake -R -K cuda=true exe torchlean cnn --device cuda --n-total 1 --steps 1

Optional flags:

• --steps N
• --batch N

See NN/Examples/Quickstart/README.md for the shared conventions in this folder.

def NN.Examples.Quickstart.SimpleCNNTrain.defaultLogJson : System.FilePath

Default JSON log path used only when the user explicitly passes --log.

def NN.Examples.Quickstart.SimpleCNNTrain.mkModel {batch : ℕ} : TorchLean.nn.M (TorchLean.nn.Sequential (Spec.Shape.dim batch (Spec.Shape.dim 1 (Spec.Shape.dim 4 (Spec.Shape.dim 4 Spec.Shape.scalar)))) (Spec.Shape.dim batch (Spec.Shape.dim 2 Spec.Shape.scalar)))

def NN.Examples.Quickstart.SimpleCNNTrain.usage : String

Command-line help for the simple CNN quickstart.

def NN.Examples.Quickstart.SimpleCNNTrain.main (args : List String) : IO Unit