Eager Session Lifecycle

Create and reset sessions, and release the intermediates their CUDA tapes own. Parameter snapshots use Lean reference counting so a reset or update in one session cannot invalidate another session.

def Runtime.Autograd.Torch.Config.forScalar {α : Type} [TorchLean.Storage α] [TensorTransfer α] (options : Config) : IO Config

Resolve a CPU-only scalar before creating either kind of recorded session. Native carriers retain the requested device, so runtime failures are not converted to fallbacks. Explicit backend profiles are still validated against the effective device.

def Runtime.Autograd.Torch.Internal.EagerSession.new {α : Type} [TorchLean.Storage α] [TensorTransfer α] (options : Config := { }) : IO (EagerSession α)

Allocate an eager session. A scalar carrier without native tensor support retains its arithmetic on CPU with a diagnostic. Native carriers still report GPU execution failures.

def Runtime.Autograd.Torch.Internal.EagerSession.releaseCudaBuffer (b : LibTorch.Buffer) : IO Unit

Release a CUDA allocation; repeated release and later finalization are safe.

def Runtime.Autograd.Torch.Internal.EagerSession.releaseCudaAnyBuffer (b : LibTorch.AnyBuffer) : IO Unit

Force-release a shape-erased CUDA buffer.

@[reducible, inline]

abbrev Runtime.Autograd.Torch.Internal.EagerSession.CudaGradMap : Type

Device-resident gradients keyed by parameter leaf ids, with each leaf's shape.

def Runtime.Autograd.Torch.Internal.EagerSession.releaseCudaGradMap (xs : CudaGradMap) : IO Unit

Release a sparse CUDA gradient map after an optimizer has consumed it.

def Runtime.Autograd.Torch.Internal.EagerSession.withCudaGradMap {β : Type} (xs : CudaGradMap) (action : CudaGradMap → IO β) : IO β

Run an action that borrows a sparse CUDA gradient map, then release every buffer in the map.

The action must not retain a gradient buffer after it returns. Cleanup also runs when the action throws, which keeps optimizer failures from leaking device memory.

def Runtime.Autograd.Torch.Internal.EagerSession.checkCudaAnyBufferSize (where_ : String) (x : LibTorch.AnyBuffer) : IO Unit

Check that a shape-erased CUDA buffer has the number of elements promised by its shape.

def Runtime.Autograd.Torch.Internal.EagerSession.resetTape {α : Type} [TorchLean.Storage α] (s : EagerSession α) : IO Unit

Discard the current forward pass and invalidate its handles. Keep parameters and RNG state.

Owned CUDA intermediates are released before the tape drops its references. Parameter leaves can refer to the current mirror or an older recorded value, so their snapshots follow Lean reference counting and remain valid in any other session that still uses them. Resetting the tape neither empties LibTorch's allocator cache nor changes optimizer history.