TorchLean CLI Facade

Small command-line parsers used by examples and model-zoo commands.

Small public command-line parsers for examples.

Use these when a runnable example needs the same compact flag convention as the model zoo.

@[reducible, inline]

abbrev TorchLean.CLI.dropDashDash (args : List String) : List String

Drop Lake's -- separator when present.

@[reducible, inline]

abbrev TorchLean.CLI.hasHelp (args : List String) : Bool

Return true when the argument list requests command help.

def TorchLean.CLI.seed (exeName : String) (args : List String) (default : ℕ := 0) : IO (ℕ × List String)

Parse --seed N, returning the selected seed and remaining arguments.

def TorchLean.CLI.natFlag? (exeName : String) (args : List String) (name : String) : IO (Option ℕ × List String)

Parse an optional natural-number flag such as --steps 200.

def TorchLean.CLI.natFlagDefault (exeName : String) (args : List String) (name : String) (default : ℕ) : IO (ℕ × List String)

Parse an optional natural-number flag and fall back to a default.

def TorchLean.CLI.positiveNatFlag (exeName : String) (args : List String) (name : String) (default : ℕ) : IO (ℕ × List String)

Parse an optional natural-number flag, fall back to a default, and require that the selected value is strictly positive.

def TorchLean.CLI.pathFlag? (exeName : String) (args : List String) (name : String) : IO (Option System.FilePath × List String)

Parse an optional path flag such as --csv data.csv.

def TorchLean.CLI.floatFlagDefault (exeName : String) (args : List String) (name : String) (default : Float) : IO (Float × List String)

Parse an optional float flag and fall back to a default.

def TorchLean.CLI.pathFlagDefault (exeName : String) (args : List String) (name : String) (default : System.FilePath) : IO (System.FilePath × List String)

Parse an optional path flag and fall back to a default path.

def TorchLean.CLI.epochBatch (exeName : String) (args : List String) (defaultEpochs defaultBatch : ℕ) : IO (NN.API.CLI.EpochBatch × List String)

Parse the --epochs E --batch N pair used by the small epoch-oriented tutorial commands.

Step-based model-zoo training commands use the ModelZoo / Trainer.TrainOptions path instead.

@[reducible, inline]

abbrev TorchLean.CLI.takeEpochBatch (args : List String) (defaultEpochs defaultBatch : ℕ) : Except String (NN.API.CLI.EpochBatch × List String)

Parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.takePositiveEpochBatch (args : List String) (exeName : String) (defaultEpochs defaultBatch : ℕ) : Except String (NN.API.CLI.EpochBatch × List String)

Parser used by epoch-oriented tutorial commands that require positive --epochs and --batch.

def TorchLean.CLI.orThrow {α : Type} (exeName : String) (result : Except String α) : IO α

Convert an Except String α into IO α with a shared executable name.

def TorchLean.CLI.requireNoArgs (exeName : String) (args : List String) : IO Unit

Require that no example-specific arguments remain after parsing.

def TorchLean.CLI.takeSeed (args : List String) (default : ℕ := 0) : Except String (ℕ × List String)

Parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.takeNatFlagOnce (args : List String) (key : String) : Except String (Option ℕ × List String)

Parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.takeNatFlagDefault (args : List String) (key : String) (default : ℕ) : Except String (ℕ × List String)

Parser used by model-zoo commands that want a natural-number flag with a default.

@[reducible, inline]

abbrev TorchLean.CLI.takePositiveNatFlagDefault (args : List String) (exeName key : String) (default : ℕ) : Except String (ℕ × List String)

Parser used by model-zoo commands that want a positive natural-number flag.

@[reducible, inline]

abbrev TorchLean.CLI.takeFloatFlagOnce (args : List String) (key : String) : Except String (Option Float × List String)

Low-level parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.takeFloatFlagDefault (args : List String) (key : String) (default : Float) : Except String (Float × List String)

Low-level parser used by model-zoo commands that want a float flag with a default.

@[reducible, inline]

abbrev TorchLean.CLI.takePositiveFloatFlagDefault (args : List String) (exeName key : String) (default : Float) : Except String (Float × List String)

Low-level parser used by model-zoo commands that require a positive float flag.

@[reducible, inline]

abbrev TorchLean.CLI.takeNonnegativeFloatFlagDefault (args : List String) (exeName key : String) (default : Float) : Except String (Float × List String)

Low-level parser used by model-zoo commands that require a nonnegative float flag.

@[reducible, inline]

abbrev TorchLean.CLI.takeFlagValueOnce (args : List String) (key : String) : Except String (Option String × List String)

Low-level parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.takeFlagValueDefault (args : List String) (key default : String) : Except String (String × List String)

Low-level parser used by model-zoo commands that want a concrete string-valued flag.

def TorchLean.CLI.takeParsedFlagDefault {α : Type} (args : List String) (key default : String) (parse : String → Except String α) : Except String (α × List String)

Low-level parser used by model-zoo commands whose string flag is decoded by a custom parser.

@[reducible, inline]

abbrev TorchLean.CLI.takePathFlagOnce (args : List String) (key : String) : Except String (Option System.FilePath × List String)

Low-level parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.takePathFlagDefault (args : List String) (key : String) (default : System.FilePath) : Except String (System.FilePath × List String)

Low-level parser used by model-zoo commands that want a concrete path with a default.

def TorchLean.CLI.takeRequiredPathFlag (args : List String) (key : String) (exeName : String := "") : Except String (System.FilePath × List String)

Low-level parser used by model-zoo commands that require a path flag to be present.

@[reducible, inline]

abbrev TorchLean.CLI.takePairedPathFlags (args : List String) (key1 key2 : String) : Except String ((Option System.FilePath × Option System.FilePath) × List String)

Low-level parser used by model-zoo commands whose two path flags must appear together.

@[reducible, inline]

abbrev TorchLean.CLI.takeBoolFlagOnce (args : List String) (key : String) : Except String (Bool × List String)

Low-level parser used by model-zoo commands that build an Except parser first.

@[reducible, inline]

abbrev TorchLean.CLI.checkNoArgs (args : List String) : Except String Unit

Low-level no-extra-arguments check for parsers that stay in Except.

@[reducible, inline]

abbrev TorchLean.CLI.hasFlagValue (args : List String) (key : String) : Bool

Check whether a flag appears with an attached value such as --log out.json.

@[reducible, inline]

abbrev TorchLean.CLI.takeStepsFlagDefault (args : List String) (default : ℕ) : Except String (ℕ × List String)