TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.API.Runtime

Runtime Selection #

Arithmetic semantics, execution mode, device, and backend-contract inspection.

source
@[reducible, inline]
abbrev TorchLean.Runtime.Config :
Type

Arithmetic semantics, execution mode, and device for a run. The record is defined with the Torch runtime; this is the name the public API uses, so user code never spells Runtime.Autograd.Torch to configure a run.

Instances For
    source
    @[reducible, inline]
    abbrev TorchLean.Runtime.ValueRef (m : Type → Type) (α : Type) [Storage α] [Context α] [Monad m] [Ops m α] (shape : Shape) :
    Type

    A shape-indexed handle to a value owned by a runtime program.

    Unlike Tensor, a ValueRef does not contain tensor elements. It names an intermediate value in an eager session or typed graph and is valid only in the program that created it.

    Instances For
      source
      def TorchLean.Runtime.linear {α : Type} [Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] (batchShape : Shape := []) {inputWidth outputWidth : ℕ} (weight : ValueRef m α [outputWidth, inputWidth]) (bias : ValueRef m α [outputWidth]) (input : ValueRef m α (batchShape.appendDim inputWidth)) :
      m (ValueRef m α (batchShape.appendDim outputWidth))

      Apply an affine map to the final axis, independently over every index in batchShape.

      Instances For

        Operation-Polymorphic Programs #

        These operations build or execute runtime programs. They consume shape-indexed references rather than materialized Tensor values, so they live under Runtime instead of the pure tensor API. Ordinary models should use nn and Trainer; this lower-level surface is useful for custom losses, verification programs, and graph-lowering tools.

        source
        def TorchLean.Runtime.ExecutionMode.cliName :
        ExecutionMode → String

        Stable command-line spelling of an execution mode.

        Instances For
          source
          def TorchLean.Runtime.ExecutionMode.parse (value : String) :
          Except String ExecutionMode

          Parse the stable command-line spelling of an execution mode.

          Instances For
            source
            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.

            Instances For
              source
              def TorchLean.Runtime.BackendContracts.planReport (config : Config) (ops : Array NN.Backend.BackendOp) :
              Except String String

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

              Instances For