Simple CNN training example

This is the image-classification companion to the small MLP tutorial.

The code is meant to look like normal model code: define the layers, choose a trainer, batch the small dataset, and call trainer.train. The shape-indexed tensors and checked training task are still there underneath, but they are not the first thing a new reader has to fight.

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 build -R -K cuda=true && lake exe torchlean cnn --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 (TorchLean.Shape.images batch 1 4 4) (TorchLean.Shape.mat batch 2))

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