Executable Module Commands

Command-line support for executable TorchLean programs, including arithmetic and device selection, help output, seed parsing, banners, and exit codes.

structure TorchLean.Module.RuntimeSelection : Type

Runtime choices parsed from the shared command-line flags.

• arithmetic : Runtime.Arithmetic

  Arithmetic semantics for this execution.

• device : NN.Backend.Device

  Requested execution device.

• showBackend : Bool

  Whether to print each backend capsule when first used.

def TorchLean.Module.instReprRuntimeSelection.repr : RuntimeSelection → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Module.instReprRuntimeSelection : Repr RuntimeSelection

def TorchLean.Module.instDecidableEqRuntimeSelection.decEq (x✝ x✝¹ : RuntimeSelection) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.Module.instDecidableEqRuntimeSelection : DecidableEq RuntimeSelection

def TorchLean.Module.RuntimeSelection.parse (arguments : List String) (defaultArithmetic : Runtime.Arithmetic := native) : Except String (RuntimeSelection × List String)

Parse the shared arithmetic, device, and backend-reporting flags.

Named devices without an installed runtime remain parseable so diagnostics can report the intended target. Runtime.Config.validateForExecution rejects such a configuration before execution.

def TorchLean.Module.RuntimeSelection.parse.go (device : NN.Backend.Device) (showBackend : Bool) (acc : List String) : List String → Except String (NN.Backend.Device × Bool × List String)

def TorchLean.Module.RuntimeSelection.toConfig (selection : RuntimeSelection) (seed : ℕ := 0) : Except String Runtime.Config

Convert parsed command-line choices to an explicit runtime configuration.

def TorchLean.Module.RuntimeSelection.log (selection : RuntimeSelection) : IO Unit

Print the selected arithmetic and device.

def TorchLean.Module.withSelectedRuntime (arguments : List String) (continuation : {α : Type} → [Storage α] → [Context α] → [ToString α] → [Runtime.FromFloat α] → (Float → α) → Runtime.Config → List String → IO Unit) : IO Unit

Parse the shared runtime flags, select executable arithmetic, and call continuation with the corresponding literal conversion and explicit runtime options.

structure TorchLean.Module.Command.RuntimeRequirements : Type

Runtime properties required by an executable command.

• device? : Option NN.Backend.Device

  Required execution device, or no device restriction.

@[instance_reducible]

instance TorchLean.Module.Command.instInhabitedRuntimeRequirements : Inhabited RuntimeRequirements

def TorchLean.Module.Command.RuntimeRequirements.applyDefaults (requirements : RuntimeRequirements) (arguments : List String) : List String

Supply required runtime flags only when the caller did not choose them explicitly.

def TorchLean.Module.Command.RuntimeRequirements.validate (requirements : RuntimeRequirements) (runtime : Runtime.Config) : Except String Unit

Reject a parsed runtime selection that conflicts with the command's requirements.

structure TorchLean.Module.Command.Config : Type

Banner, success-message, and flushing configuration for an executable command.

• banner? : Option (Runtime.Config → String)

  Optional banner to print before executing the program.

• usage? : Option String

  Command-specific help text; the generic runtime help is used when absent.

• flush : Bool

  Flush stdout after printing the banner, when present.

• printSuccess : Bool

  Print "{exeName}: ok" after successful execution.

• runtime : RuntimeRequirements

  Device requirements imposed by this command.

@[instance_reducible]

instance TorchLean.Module.Command.instInhabitedConfig : Inhabited Config

def TorchLean.Module.Command.Config.printBanner (config : Config) (runtime : Runtime.Config) : IO Unit

Print the configured executable banner, if one was supplied.

def TorchLean.Module.Command.usage (exeName : String) : String

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

def TorchLean.Module.Command.run (exeName : String) (arguments : List String) (action : Runtime.Config → List String → IO Unit) (config : Config := { }) : 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 Runtime.Config, so model initialization and training observe the same seed.