TorchLean Public Checkpoints

Checkpoint loading and saving operations for exact Float bit payloads.

def TorchLean.Checkpoint.loadParamBits {paramShapes : List Shape} (path : System.FilePath) : IO (nn.ParamTensors Float paramShapes)

Load a JSON checkpoint containing exact Float.toBits parameter values.

The loader checks the saved tensor pack against the model's parameter shapes. Examples such as gpt2_saved use this boundary for inference from saved weights.

def TorchLean.Checkpoint.loadModelParamBits {σ τ : Shape} (model : nn.Sequential σ τ) (path : System.FilePath) : IO (nn.ParamTensors Float (nn.paramShapes model))

Load a JSON checkpoint containing exact Float.toBits parameter values for one checked model.

This is the model-specialized companion to loadParamBits: callers can hand it the model they are about to evaluate instead of repeating paramShapes := nn.paramShapes model.

def TorchLean.Checkpoint.toRuntimeParams {paramShapes : List Shape} (ps : nn.ParamTensors Float paramShapes) : IO (Runtime.Autograd.Torch.ParamList Float paramShapes)

Turn loaded parameter tensors into runtime parameter handles.

Use this when an example wants inference-only execution without constructing a trainer first.

def TorchLean.Checkpoint.loadModuleParamBits {paramShapes inputShapes : List Shape} (m : Module.ScalarModule Float paramShapes inputShapes) (path : System.FilePath) : IO Unit

Load exact Float.toBits parameters into an existing runtime module.

def TorchLean.Checkpoint.loadModelIntoModule {σ τ : Shape} (model : nn.Sequential σ τ) (m : Module.ScalarModule Float (nn.paramShapes model) [σ, τ]) (path : System.FilePath) : IO Unit

Load exact Float.toBits parameters into an existing runtime module attached to one checked model.

The model determines the parameter and input shape indices at the call site.

def TorchLean.Checkpoint.loadModelIntoModuleIfSome {σ τ : Shape} (model : nn.Sequential σ τ) (m : Module.ScalarModule Float (nn.paramShapes model) [σ, τ]) (path? : Option System.FilePath) : IO Unit

Load exact Float.toBits parameters into a model-attached runtime module when a checkpoint path is present.

def TorchLean.Checkpoint.saveModuleParamBits {paramShapes inputShapes : List Shape} (m : Module.ScalarModule Float paramShapes inputShapes) (path : System.FilePath) : IO Unit

Save a runtime module's parameters as exact Float.toBits JSON.

def TorchLean.Checkpoint.saveModelIntoPathIfSome {σ τ : Shape} (model : nn.Sequential σ τ) (m : Module.ScalarModule Float (nn.paramShapes model) [σ, τ]) (path? : Option System.FilePath) : IO Unit

Save a model-attached runtime module's exact Float.toBits parameters when an output path is present, and print the standard confirmation line.