Runtime Modules and Executable Entrypoints

Scalar-module instantiation, runtime initialization, CLI execution config parsing, and executable main helpers.

Model constructors (re-export)

This namespace re-exports ready-made model constructors (MLP/CNN/ResNet18/etc.) for runnable examples and integration checks.

For compositional building blocks, prefer API.TorchLean.NN and API.TorchLean.Layers.

ScalarModule API (Session-Like Interface)

The ScalarModule interface is the TorchLean equivalent of "instantiate a model, then do forward, backward, and optimizer steps" in an imperative runtime.

This section mostly re-exports Runtime.Autograd.TorchLean.Module.* and adds small CLI-friendly helpers (Module.withModule / Module.withModuleRuntime) that select dtype/backend from flags.

def NN.API.TorchLean.Module.instantiateWithOptions {α : Type} [Semantics.Scalar α] [DecidableEq Spec.Shape] [Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α] {paramShapes inputShapes : List Spec.Shape} (defn : ScalarModuleDef paramShapes inputShapes) (cast : Float → α) (opts : Options) : IO (ScalarModule α paramShapes inputShapes)

Instantiate a ScalarModuleDef under explicit Torch options (backend, fastKernels, useGpu, etc.).

This is the most direct "runtime" entrypoint (used by the CPU/CUDA example binaries), since it threads the same options record all the way down to the eager tape / CUDA tape selection.

The shorter instantiate entrypoint selects the backend and then uses default runtime options.

def NN.API.TorchLean.Module.instantiateFloatWithRuntimePlanOptions {paramShapes inputShapes : List Spec.Shape} (defn : ScalarModuleDef paramShapes inputShapes) (opts : Options) (plan : RuntimeInit.Plan paramShapes) : IO (ScalarModule Float paramShapes inputShapes)

Instantiate a Float module with runtime-side parameter initializers.

This is the public runtime-initialization entrypoint. The initializer plan is indexed by the same paramShapes list as the module, so Lean checks that every parameter has exactly one initializer. In CUDA mode, supported initializers allocate device buffers directly instead of first constructing every parameter as a large nested Lean tensor.

def NN.API.TorchLean.Module.instantiateFloatWithRuntimeInitOptions {paramShapes inputShapes : List Spec.Shape} (defn : ScalarModuleDef paramShapes inputShapes) (opts : Options) (inits : List RuntimeInit.FloatInit) : IO (ScalarModule Float paramShapes inputShapes)

List-based wrapper for checkpoint/JSON boundaries.

If the caller has a statically known parameter list, prefer instantiateFloatWithRuntimePlanOptions; this wrapper checks the list length before applying it.

structure NN.API.TorchLean.Module.ExecConfig : Type

Execution configuration parsed from CLI flags.

Supported flags (parsed by ExecConfig.parseAndStrip):

• --dtype ... / --float32-mode ... (see NN.API.DType)
• --backend eager|compiled
• --cpu / --cuda (eager device selection)
• --fast-kernels (eager-only performance hooks, no effect on compiled backend)
• --fast-gpu-matmul-precision fp32|fp64 (fast-kernel CUDA matmul precision)

• dtype : DType

  Scalar dtype selection.

• backend : Backend

  Execution backend selection.

• useGpu : Bool

  Eager execution device selector.

  When true and backend = .eager, TorchLean uses the CUDA tape backend.

• fastKernels : Bool

  Enable runtime-only eager fast kernels (tight-loop implementations for a few hot ops).

• fastGpuMatmulPrecision : GpuMatmulPrecision

  GPU precision for fast-kernel matmul over Lean Float tensors.

def NN.API.TorchLean.Module.instReprExecConfig.repr : ExecConfig → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.TorchLean.Module.instReprExecConfig : Repr ExecConfig

@[implicit_reducible]

instance NN.API.TorchLean.Module.instDecidableEqExecConfig : DecidableEq ExecConfig

def NN.API.TorchLean.Module.instDecidableEqExecConfig.decEq (x✝ x✝¹ : ExecConfig) : Decidable (x✝ = x✝¹)

def NN.API.TorchLean.Module.ExecConfig.parseBackend (v : String) : Except String Backend

Parse a backend selector string into a runtime Backend.

def NN.API.TorchLean.Module.ExecConfig.parseFastGpuMatmulPrecision (v : String) : Except String GpuMatmulPrecision

Parse a fast-kernel CUDA matmul precision selector.

def NN.API.TorchLean.Module.ExecConfig.parseAndStripWithDefaultDType (args : List String) (defaultDType : DType) : Except String (ExecConfig × List String)

Parse CLI flags handled by ExecConfig and return (cfg, rest).

Consumed flags:

• --backend eager|compiled (at most once),
• --cpu / --cuda (boolean flags; last one wins; removed from rest),
• --fast-kernels (boolean flag; removed from rest).
• --fast-gpu-matmul-precision fp32|fp64 (at most once).

All dtype/Float32 selection flags are delegated to DType.parseAndStripWithDefault.

Default dtype policy:

• If the user does not specify --dtype / --float32-mode and --cuda is present, default to dtype=float (CUDA eager supports Float upload/download).
• Otherwise default to dtype=float32 (executable IEEE-754 float32 semantics).

def NN.API.TorchLean.Module.ExecConfig.parseAndStripWithDefaultDType.go (useGpu fastKernels : Bool) (acc : List String) : List String → Bool × Bool × List String

def NN.API.TorchLean.Module.ExecConfig.toOptions (cfg : ExecConfig) (seed : ℕ := 0) : Options

Convert a parsed CLI execution config to runtime Options.

def NN.API.TorchLean.Module.ExecConfig.parseAndStrip (args : List String) : Except String (ExecConfig × List String)

Parse CLI flags with the standard TorchLean default dtype policy.

def NN.API.TorchLean.Module.ExecConfig.log (cfg : ExecConfig) : IO Unit

Log the chosen execution config to stdout for reproducible runs.

def NN.API.TorchLean.Module.withRuntime (args : List String) (k : {α : Type} → [Semantics.Scalar α] → [DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → (Float → α) → Options → List String → IO Unit) : IO Unit

Parse runtime flags (--dtype, --backend, --cpu|--cuda, --fast-kernels, --fast-gpu-matmul-precision) and choose an executable scalar α, then call k with:

• cast : Float → α for building inputs from literals
• opts : Options selecting the backend/kernel mode
• rest : List String containing the remaining CLI arguments

This is useful for scripts that need to build a dataset/loader (and maybe determine shapes/batch sizes) before instantiating a concrete ScalarModuleDef.

def NN.API.TorchLean.Module.withModule {paramShapes inputShapes : List Spec.Shape} (defn : ScalarModuleDef paramShapes inputShapes) (args : List String) (k : {α : Type} → [inst : Semantics.Scalar α] → [inst_1 : DecidableEq Spec.Shape] → [ToString α] → (Float → α) → ScalarModule α paramShapes inputShapes → List String → IO Unit) : IO Unit

Instantiate a ScalarModuleDef under CLI runtime flags (--dtype, --backend, --cpu|--cuda, --fast-kernels, --fast-gpu-matmul-precision), then call a continuation.

This provides the cast function Float → α so call sites can build inputs from float literals.

def NN.API.TorchLean.Module.withModuleRuntime {paramShapes inputShapes : List Spec.Shape} (defn : ScalarModuleDef paramShapes inputShapes) (args : List String) (k : {α : Type} → [inst : Semantics.Scalar α] → [inst_1 : DecidableEq Spec.Shape] → [ToString α] → [Runtime.Scalar α] → ScalarModule α paramShapes inputShapes → List String → IO Unit) : IO Unit

Like withModule, but also provides an API.Runtime.Scalar α instance (for numeric literals).

Executable main Helpers

TorchLean has a lot of pure, type-indexed code (models live in Type 2), but runnable scripts still want a "single entrypoint" that handles:

• parsing --seed,
• selecting an executable dtype/backend/device from flags,
• seeding TorchLean's global RNG stream (API.rand) so nn.freshSeed/nn.withModel are deterministic.

structure NN.API.TorchLean.Module.RunOptions : Type

Options for TorchLean.Module.run (banner printing, trailing ok, etc.).

• banner? : Option (Options → String)

  Optional banner to print before executing the program.

• flush : Bool

  Flush stdout after printing the banner (if present).

• printOk : Bool

  Print "{exeName}: ok" on success.

@[implicit_reducible]

instance NN.API.TorchLean.Module.instInhabitedRunOptions : Inhabited RunOptions

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

Print the configured executable banner, if one was supplied.

inductive NN.API.TorchLean.Module.RunAction : Type 1

How run should select the scalar backend for an executable.

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

  Allow --dtype selection (the continuation must work for all executable scalar backends).

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

  Force the scalar backend to builtin Float (useful for Float-only IO bridges / CUDA upload paths).

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

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

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

CLI entrypoint helper for executable main functions.

This parses:

• --seed N (via API.CLI.takeSeed), and
• runtime execution flags (--dtype, --float32-mode, --backend, --cpu|--cuda, --fast-kernels, --fast-gpu-matmul-precision), then executes the chosen RunAction.

It also seeds TorchLean's global RNG stream (API.rand) so code that draws init seeds via API.nn.freshSeed/API.nn.withModel is deterministic by default, matching the PyTorch pattern of calling torch.manual_seed once in main.