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.

• execution : Runtime.Autograd.Torch.ExecutionMode

  Immediate or typed-graph 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

@[instance_reducible]

instance TorchLean.Module.instDecidableEqRuntimeSelection : DecidableEq RuntimeSelection

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

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

Parse the shared arithmetic, execution, 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, execution strategy, 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.

• execution? : Option Runtime.Autograd.Torch.ExecutionMode

  Required execution strategy, or no execution-strategy 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 or execution-mode 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.

inductive TorchLean.Module.Command.Action : Type 1

How an executable command chooses its arithmetic semantics.

• selectedArithmetic (continuation : {α : Type} → [Storage α] → [Context α] → [ToString α] → [Runtime.FromFloat α] → (Float → α) → Runtime.Config → List String → IO Unit) : Action

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

• native (continuation : Runtime.Config → List String → IO Unit) : Action

  Run a command fixed to native arithmetic rather than exposing arithmetic selection.

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 : Action) (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 either execution mode observe the same seed.