Runtime Selection

Dtype, backend, device, and runtime-selection helpers.

@[reducible, inline]

abbrev TorchLean.Runtime.Backend : Type

Runtime execution strategy: eager evaluation or compiled graph execution.

@[reducible, inline]

abbrev TorchLean.Runtime.Device : Type

Physical or logical device selected for runtime execution.

def TorchLean.Runtime.Device.parse (value : String) : Except String Device

Parse a public device selector. auto chooses the portable CPU runtime; every other value is validated against the devices known to the backend registry.

def TorchLean.Runtime.runFloat (exeName : String) (args : List String) (banner : Options → String) (k : Options → List String → IO Unit) (printOk : Bool := true) : IO UInt32

Parse the usual TorchLean runtime flags and run a Float callback.

Examples should use this instead of calling TorchLean.Module.run directly; that lower-level dispatcher is what backs this wrapper.

def TorchLean.Runtime.runCudaFloat (exeName : String) (args : List String) (banner : Options → String) (k : Options → List String → IO Unit) (printOk : Bool := true) : IO UInt32

Run a Float command on CUDA, adding --device cuda when no device was supplied.

def TorchLean.Runtime.runCudaEagerFloat (exeName : String) (args : List String) (banner : Options → String) (k : Options → List String → IO Unit) (printOk : Bool := true) : IO UInt32

Run a Float command on the eager CUDA runtime.

def TorchLean.Runtime.parseArgs (args : List String) (defaultDType : DType := DType.float) : Except String (Options × List String)

Parse the standard TorchLean runtime flags and return the resulting Options.

Non-polymorphic sibling of Runtime.withOptions: examples that always run at Float can still parse --device, --backend, and --dtype without exposing a polymorphic callback.

def TorchLean.Runtime.BackendContracts.profileForOptions (opts : Options) : NN.Backend.BackendProfile

Backend-contract profile corresponding to the selected runtime options.

def TorchLean.Runtime.BackendContracts.planReport (opts : Options) (ops : List NN.Backend.BackendOp) : Except String String

Plan operations under the runtime-selected backend-contract profile.

def TorchLean.Runtime.BackendContracts.printPlan (opts : Options) (ops : List NN.Backend.BackendOp) : IO Unit

Print the selected backend capsules for operations.

def TorchLean.Runtime.withOptions (args : List String) (k : {α : Type} → [Context α] → [DecidableEq Spec.Shape] → [ToString α] → [FromFloat α] → (Float → α) → Options → List String → IO Unit) : IO Unit

Run an example under the selected runtime and pass through the parsed runtime options.

Use this when an example needs to inspect --backend, --device, or similar flags after TorchLean has selected the scalar backend.

def TorchLean.Runtime.withOptionsScalar (args : List String) (k : {α : Type} → [Context α] → [DecidableEq Spec.Shape] → [ToString α] → [FromFloat α] → Options → List String → IO Unit) : IO Unit

Run an example under the selected runtime and pass through runtime options when the callback does not need an explicit Float-cast function.

def TorchLean.Runtime.runWithDType (title : String) (args : List String) (k : {α : Type} → [Context α] → [DecidableEq Spec.Shape] → [ToString α] → [FromFloat α] → IO Unit) : IO Unit

Run a verification or demo command under the selected runtime dtype.

Banner-printing runtime dispatcher matching the convention used by lake exe verify -- ... commands.