API CLI Helpers

Small command-line parsers shared by examples, verification tools, and public facade helpers.

This module stays independent of tensors and runtime modules so lightweight artifact checkers can reuse the CLI surface without importing the full public API.

def NN.API.CLI.orThrow {α : Type} (x : Except String α) : IO α

Lift a shared CLI parser result into IO.userError.

def NN.API.CLI.takeFlagValueOnce (args : List String) (key : String) : Except String (Option String × List String)

Strip at most one occurrence of a --key flag from an argument list.

Accepted forms:

• --key value
• --key=value

def NN.API.CLI.takeFlagValueOnce.go (eqPrefix keyTok : String) : List String → Option String → List String → Except String (Option String × List String)

def NN.API.CLI.takeFlagValueDefault (args : List String) (key default : String) : Except String (String × List String)

Parse an optional string-valued flag and fall back to a provided default.

Use this when a command parser wants a concrete string immediately rather than an optional override.

def NN.API.CLI.takeRequiredFlagValue (args : List String) (key : String) (missing? : Option String := none) : Except String (String × List String)

Parse a required string-valued flag and return the remaining arguments.

def NN.API.CLI.flagValue? (args : List String) (key : String) : Except String (Option String)

Look up a string-valued flag without returning the remaining arguments.

This is useful for command shapes that support optional overrides but do not otherwise need a left-to-right consuming parser. Accepted forms are the same as takeFlagValueOnce: --key value and --key=value.

def NN.API.CLI.requireFlagValue (args : List String) (key : String) : Except String String

Require a string-valued flag, accepting both --key value and --key=value.

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

Parse an optional string-valued flag, fall back to a provided default spelling when absent, and decode the selected spelling with a caller-supplied parser.

This is useful for enum-like CLI flags whose valid strings remain command-specific.

def NN.API.CLI.hasFlagValue (args : List String) (key : String) : Bool

Return true when args contains --key value or --key=value.

def NN.API.CLI.stripFlagValues (args keys : List String) : List String

Remove every occurrence of a string-valued flag, accepting both --key value and --key=value.

This is for wrapper commands that own a flag locally and forward the remaining arguments to another tool. It deliberately does not reject duplicates; the wrapper's local parser decides whether a duplicated flag is an error.

def NN.API.CLI.stripFlagValues.go (keys : List String) : List String → List String

def NN.API.CLI.takeBoolFlagOnce (args : List String) (key : String) : Except String (Bool × List String)

Remove a no-value boolean flag once, returning whether it appeared.

partial def NN.API.CLI.takeBoolFlagOnce.go (keyTok : String) : List String → Bool → List String → Except String (Bool × List String)

def NN.API.CLI.dropDashDash (args : List String) : List String

Drop the leading -- separator commonly used with lean --run.

def NN.API.CLI.hasHelp (args : List String) : Bool

Return true when the argument list requests command help.

def NN.API.CLI.requireNoArgs (args : List String) : Except String Unit

Fail if there are any unconsumed CLI arguments.

def NN.API.CLI.takePositionalOnce (args : List String) : Except String (Option String × List String)

Take at most one positional argument, leaving flags untouched.

This is useful for commands with a single optional artifact path plus named flags. A second positional argument is reported as an error instead of being silently ignored.

def NN.API.CLI.takePositionalOnce.go : List String → Option String → List String → Except String (Option String × List String)

def NN.API.CLI.takePositionalDefault (args : List String) (default : String) : Except String (String × List String)

Take one optional positional argument and fall back to default when it is absent.

def NN.API.CLI.defaultPathFlagFromPositional (args : List String) (key default : String) : List String

Normalize commands that accept either a positional path or a named path flag.

If --key / --key=... is already present, the argument list is returned unchanged. Otherwise the first positional argument is rewritten to --key=<path>. If there is no positional path, the provided default path is inserted.

def NN.API.CLI.takeNatFlagOnce (args : List String) (key : String) : Except String (Option Nat × List String)

Like takeFlagValueOnce, but parse the value as a Nat.

def NN.API.CLI.takeNatFlagDefault (args : List String) (key : String) (default : Nat) : Except String (Nat × List String)

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

def NN.API.CLI.takePositiveNatFlagDefault (args : List String) (exeName key : String) (default : Nat) : Except String (Nat × List String)

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

def NN.API.CLI.parseDecimalDigit? (c : Char) : Option Nat

Parse one ASCII decimal digit.

def NN.API.CLI.parseNatDigits? (s : String) : Option Nat

Parse a nonempty string of ASCII decimal digits.

def NN.API.CLI.parseFloatLit (s : String) : Option Float

Parse a signed decimal float literal.

The primary path accepts the same numeric syntax as Lean.Json, including scientific notation. The fallback accepts the CLI-friendly decimal form 1..

def NN.API.CLI.takeFloatFlagOnce (args : List String) (key : String) : Except String (Option Float × List String)

Like takeFlagValueOnce, but parse the value as a Float.

def NN.API.CLI.takeFloatFlagDefault (args : List String) (key : String) (default : Float) : Except String (Float × List String)

Parse an optional floating-point flag and fall back to the provided default.

def NN.API.CLI.takeRequiredFloatFlag (args : List String) (key : String) (missing? : Option String := none) : Except String (Float × List String)

Parse a required floating-point flag and return the remaining arguments.

def NN.API.CLI.parseBoolLit (s : String) : Option Bool

Parse a CLI boolean value. Accepted spellings are true, false, 1, and 0.

def NN.API.CLI.takeBoolValueFlagOnce (args : List String) (key : String) : Except String (Option Bool × List String)

Like takeFlagValueOnce, but parse the value as a boolean.

def NN.API.CLI.takeBoolValueFlagDefault (args : List String) (key : String) (default : Bool) : Except String (Bool × List String)

Parse an optional boolean-valued flag and fall back to the provided default.

def NN.API.CLI.takeBoolFlagOptionalValueOnce (args : List String) (key : String) : Except String (Option Bool × List String)

Remove a boolean flag that may be written either as a bare switch or with an explicit value.

Accepted forms:

• --key
• --key=true
• --key=false
• --key true
• --key false

When --key is followed by a non-boolean token, the flag is treated as a bare switch and the next token is left for the caller. Duplicate occurrences are rejected.

partial def NN.API.CLI.takeBoolFlagOptionalValueOnce.go (keyTok eqPrefix : String) (args : List String) (seen : Option Bool) (acc : List String) : Except String (Option Bool × List String)

def NN.API.CLI.takeBoolFlagOptionalValueDefault (args : List String) (key : String) (default : Bool) : Except String (Bool × List String)

Parse a bare-or-valued boolean flag and fall back to the provided default.

def NN.API.CLI.takePositiveFloatFlagDefault (args : List String) (exeName key : String) (default : Float) : Except String (Float × List String)

Parse an optional floating-point flag, fall back to the provided default, and require that the selected value is strictly positive.

def NN.API.CLI.takeNonnegativeFloatFlagDefault (args : List String) (exeName key : String) (default : Float) : Except String (Float × List String)

Parse an optional floating-point flag, fall back to the provided default, and require that the selected value is nonnegative.

def NN.API.CLI.takePathFlagOnce (args : List String) (key : String) : Except String (Option System.FilePath × List String)

Like takeFlagValueOnce, but return the value as a System.FilePath.

def NN.API.CLI.takePathFlagDefault (args : List String) (key : String) (default : System.FilePath) : Except String (System.FilePath × List String)

Parse an optional path flag and fall back to the provided default path.

Use this when an example parser wants a concrete path immediately instead of an optional override.

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

Parse a required path flag such as --data-file corpus.txt.

The error message includes exeName when provided.

def NN.API.CLI.takePairedPathFlags (args : List String) (key1 key2 : String) : Except String ((Option System.FilePath × Option System.FilePath) × List String)

Parse two optional path flags that must appear together if either one is present.

This is useful for paired artifacts such as tokenizer vocab/merge files, where a single path is not meaningful on its own.

structure NN.API.CLI.EpochBatch : Type

Common training flags for epoch-oriented loader/tutorial commands: --epochs and --batch.

• epochs : Nat

  Number of epochs to train for.

• batch : Nat

  Batch size.

def NN.API.CLI.takeEpochBatch (args : List String) (defaultEpochs defaultBatch : Nat) : Except String (EpochBatch × List String)

Parse optional --epochs and --batch flags for the epoch-oriented tutorial helpers.

Returns the parsed values (falling back to the provided defaults) and the remaining args.

def NN.API.CLI.takePositiveEpochBatch (args : List String) (exeName : String) (defaultEpochs defaultBatch : Nat) : Except String (EpochBatch × List String)

Parse optional --epochs and --batch flags for the epoch-oriented tutorial helpers, fall back to the provided defaults, and require that both selected values are strictly positive.

def NN.API.CLI.takeStepsFlagDefault (args : List String) (default : Nat) : Except String (Nat × List String)

Parse an optional --steps flag and fall back to the provided default.

def NN.API.CLI.takeSeed (args : List String) (default : Nat := 0) : Except String (Nat × List String)

Parse an optional --seed flag (defaults to the provided value).