TorchLean Runtime Facade

Runtime dtype, backend, device, and scalar-polymorphic entrypoints.

@[reducible, inline]

abbrev TorchLean.Runtime.DType : Type

Scalar type choice for runnable executables.

This is a runtime selection mechanism used by example programs; the core library itself is parametric in the scalar type α.

PyTorch Mapping

This corresponds loosely to choosing dtype= in PyTorch, but with additional "proof-only" variants:

• .float uses Lean's builtin Float (executable, but its IEEE-754 behavior is trusted),
• .float32 uses TorchLean's float32 model (either proof-only or executable),
• .complex uses TorchLean's parametric complex scalar over a float32 backend,
• .real uses ℝ (proof-only; not executable).

@[reducible, inline]

abbrev TorchLean.Runtime.DType.float : DType

@[reducible, inline]

abbrev TorchLean.Runtime.DType.float32 (cfg : NN.API.Float32Config := { }) : DType

@[reducible, inline]

abbrev TorchLean.Runtime.DType.complex (cfg : NN.API.Float32Config := { }) : DType

@[reducible, inline]

abbrev TorchLean.Runtime.DType.real : DType

Runtime-facing scalar classes.

Most ordinary TorchLean code should let Trainer provide these instances implicitly. A few advanced demos use Runtime.withOptions / Runtime.withOptionsNoCast to run the same code under a CLI-selected scalar backend. The classes live under TorchLean.Runtime so the root namespace stays focused on the model/data/trainer surface rather than on backend evidence.

@[reducible, inline]

abbrev TorchLean.Runtime.Scalar (α : Type) : Type

Runtime scalar support for executable TorchLean examples.

Advanced examples use this when they choose a scalar backend or write runtime-polymorphic code over the selected execution mode.

@[reducible, inline]

abbrev TorchLean.Runtime.SemanticScalar (α : Type) : Type

Mathematical scalar operations used by TorchLean model and loss definitions.

This is the semantic scalar class used by runtime-selected examples and advanced verification/demo entrypoints.

@[reducible, inline]

abbrev TorchLean.Runtime.TensorScalar (α : Type) : Type

Scalar operations needed to build and manipulate shape-indexed TorchLean tensors.

@[reducible, inline]

abbrev TorchLean.Runtime.Backend : Type

Execution backend for the Torch-style front-end.

• .eager: build and execute a runtime tape directly (imperative, PyTorch-like).
• .compiled: record typed IR and run a compiled tape (proof-friendly path, see Torch.LinkedSession / TorchLean.Session).

This is not a CUDA Graph selector. CUDA is controlled by Options.device on the eager backend; CUDA Graph capture/replay will require a distinct persistent-buffer backend.

@[reducible, inline]

abbrev TorchLean.Runtime.Backend.eager : Backend

@[reducible, inline]

abbrev TorchLean.Runtime.Backend.compiled : Backend

@[reducible, inline]

abbrev TorchLean.Runtime.Device : Type

Execution device selector (PyTorch comparison: cpu vs cuda).

Current scope:

• eager backend only: selects whether the hidden tape is CPU (Runtime.Autograd.Tape) or CUDA (Runtime.Autograd.Cuda.Tape),
• compiled backend is unchanged (proof semantics / typed IR are device-agnostic).

@[reducible, inline]

abbrev TorchLean.Runtime.Device.cpu : Device

@[reducible, inline]

abbrev TorchLean.Runtime.Device.cuda : Device

def TorchLean.Runtime.ofFloat {α : Type} [Scalar α] (x : Float) : α

Generic host-float injection for TorchLean scalar backends.

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

Run a Float-only command with the standard TorchLean runtime flags.

This is the public spelling for the common "parse --cpu/--cuda/--backend, then run a concrete Float callback" boundary. Examples should use this or ModelZoo.runFloat instead of calling TorchLean.Module.run directly; the latter is the runtime dispatcher that backs this facade.

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.

This is the non-polymorphic sibling of Runtime.withOptions: examples that always execute at Float but still need --cpu, --cuda, --backend, or --dtype can parse the usual runtime flags without exposing a polymorphic callback in user-facing code.

def TorchLean.Runtime.withSelected (args : List String) (k : {α : Type} → [SemanticScalar α] → [DecidableEq Shape] → [ToString α] → [Scalar α] → (Float → α) → List String → IO Unit) : IO Unit

Run an advanced scalar-polymorphic example under the dtype/backend selected by the usual TorchLean CLI flags.

The callback receives:

• cast, for turning Float literals into the selected executable scalar type,
• rest, the arguments left after runtime flags are stripped.

Prefer Trainer for model training. Use this only for demos that really need the selected scalar type in their own code, for example small autograd/runtime walkthroughs.

def TorchLean.Runtime.withSelectedNoCast (args : List String) (k : {α : Type} → [SemanticScalar α] → [DecidableEq Shape] → [ToString α] → [Scalar α] → List String → IO Unit) : IO Unit

Run an advanced scalar-polymorphic example under the selected runtime when the callback does not need a Float-cast function.

Prefer Runtime.withOptionsNoCast when the callback also needs parsed runtime options. This exists for the rare case where only the selected scalar/backend instances and remaining CLI arguments matter.

def TorchLean.Runtime.withOptions (args : List String) (k : {α : Type} → [SemanticScalar α] → [DecidableEq Shape] → [ToString α] → [Scalar α] → (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 advanced example needs to inspect --backend, --cuda, or similar flags after TorchLean has selected the scalar backend.

def TorchLean.Runtime.withOptionsNoCast (args : List String) (k : {α : Type} → [SemanticScalar α] → [DecidableEq Shape] → [ToString α] → [Scalar α] → Options → List String → IO Unit) : IO Unit

Run an advanced 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} → [SemanticScalar α] → [DecidableEq Shape] → [ToString α] → [Scalar α] → IO Unit) : IO Unit

Run a verification/demo entrypoint under the selected runtime dtype.

This is the banner-printing sibling of withSelected; it matches the convention used by lake exe verify -- ... commands.