TorchLean Example Runner

Executable root for the torchlean example runner.

Each example keeps its own namespace, and this module selects which one to run from a subcommand argument such as mlp or gpt2.

def NN.Examples.Models.Runner.usage : String

def NN.Examples.Models.Runner.prefixFlagTakesValue (a : String) : Bool

Runtime flags that consume the following command-line token.

def NN.Examples.Models.Runner.splitCommandArgs? (args : List String) : Option (List String × String × List String)

Split CLI arguments into (prefixFlags, command, commandArgs).

We allow "global" runtime flags before the command name so users can write either:

• torchlean mlp --device cpu, or
• torchlean --device cpu mlp.

def NN.Examples.Models.Runner.splitCommandArgs?.go (prefixRev : List String) : List String → Option (List String × String × List String)

def NN.Examples.Models.Runner.hasDeviceFlag : List String → Bool

Detect whether the command line already selects a runtime device.

def NN.Examples.Models.Runner.readPromptLine : IO String

Read one line, treating EOF as the default answer.

partial def NN.Examples.Models.Runner.askDevice : IO (List String)

Ask for the device in the interactive runtime chooser.

def NN.Examples.Models.Runner.chooseRuntimeArgs (args : List String) : IO (List String)

Fill in missing runtime choices interactively.

The chooser is explicit (--choose) so scripts, tests, and CI never block waiting for stdin.

def NN.Examples.Models.Runner.stripRunnerFlag (flag : String) : List String → List String

Strip top-level runner flags that are not meant for individual examples.

def NN.Examples.Models.Runner.runCmd (cmd : String) (args : List String) : IO UInt32

def NN.Examples.Models.Runner.main (args : List String) : IO UInt32