Executable Module Commands

Command-line support for executable TorchLean programs, including help output, seed parsing, banners, and exit codes. Module construction and device selection are defined in NN.API.Module.Execution.

structure TorchLean.Module.RunOptions : Type

Options for TorchLean.Module.run (banner printing, trailing success message, and flushing).

• banner? : Option (Options → String)

  Optional banner to print before executing the program.

• flush : Bool

  Flush stdout after printing the banner, when present.

• printOk : Bool

  Print "{exeName}: ok" on success.

@[implicit_reducible]

instance TorchLean.Module.instInhabitedRunOptions : Inhabited RunOptions

def TorchLean.Module.RunOptions.printBanner (o : RunOptions) (opts : Options) : IO Unit

Print the configured executable banner, if one was supplied.

inductive TorchLean.Module.RunAction : Type 1

How run should select the scalar backend for an executable.

• scalarPolymorphic (k : {α : Type} → [Context α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.FromFloat α] → (Float → α) → Options → List String → IO Unit) : RunAction

  Allow dtype selection; the continuation must work for every executable scalar backend.

• float (k : Options → List String → IO Unit) : RunAction

  Force builtin Float, as required by Float-only IO bridges and CUDA upload paths.

def TorchLean.Module.runUsage (exeName : String) : String

Generic help text for executables built on TorchLean.Module.run.

def TorchLean.Module.run (exeName : String) (args : List String) (action : RunAction) (runOpts : RunOptions := { }) : IO UInt32

Run a TorchLean executable after parsing the shared seed and runtime flags.

The selected seed initializes TorchLean's global random stream and is also stored in Options, so model initialization and the eager or compiled session observe the same seed.