Cache Map

@[reducible, inline]

abbrev Lake.CacheMap : Type

Maps an input hash to a structure of output artifact content hashes.

These mappings are stored in a per-package JSON Lines file in the Lake cache.

Equations

• Lake.CacheMap = Std.HashMap Lake.Hash Lean.Json

def Lake.CacheMap.schemaVersion : String

The current version of the input-to-output mappings file format.

Equations

• Lake.CacheMap.schemaVersion = "2025-09-10"

def Lake.CacheMap.parse (inputName contents : String) : LoggerIO CacheMap

Parse a Cache from a JSON Lines string.

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheMap.load (file : System.FilePath) : LogIO CacheMap

Loads a CacheMap from a JSON Lines file. Errors if the the file is ill-formatted or the read fails for other reasons.

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheMap.load? (file : System.FilePath) : LogIO (Option CacheMap)

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheMap.updateFile (file : System.FilePath) (cache : CacheMap) : LogIO Unit

Save a CacheMap to a JSON Lines file. Entries already in the file but not in the map will not be removed.

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheMap.writeFile (file : System.FilePath) (cache : CacheMap) : LogIO Unit

Write a CacheMap to a JSON Lines file.

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheMap.get? (inputHash : Hash) (cache : CacheMap) : Option Lean.Json

Returns the output data associated with the input hash in the cache.

Equations

• Lake.CacheMap.get? inputHash cache = Std.HashMap.get? cache inputHash

def Lake.CacheMap.insertCore (inputHash : Hash) (val : Lean.Json) (cache : CacheMap) : CacheMap

Associate output data (as JSON) with the given the input hash.

Equations

• Lake.CacheMap.insertCore inputHash val cache = Std.HashMap.insert cache inputHash val

@[inline]

def Lake.CacheMap.insert {α : Type u_1} [Lean.ToJson α] (inputHash : Hash) (val : α) (cache : CacheMap) : CacheMap

Associate output data with the given the input hash.

Equations

• Lake.CacheMap.insert inputHash val cache = Lake.CacheMap.insertCore inputHash (Lean.toJson val) cache

def Lake.CacheMap.collectOutputDescrs (map : CacheMap) : LogIO (Array ArtifactDescr)

Extract each output from their structured data into a flat array of artifact descriptions.

Equations

• One or more equations did not get rendered due to their size.

Cache Ref

@[reducible, inline]

abbrev Lake.CacheRef : Type

A mutable reference to a CacheMap.

Equations

• Lake.CacheRef = IO.Ref Lake.CacheMap

@[inline]

def Lake.CacheRef.mk (init : CacheMap := ∅) : BaseIO CacheRef

Equations

• Lake.CacheRef.mk init = IO.mkRef init

@[inline]

def Lake.CacheRef.get? (inputHash : Hash) (cache : CacheRef) : BaseIO (Option Lean.Json)

Returns the output data associated with the input hash in the cache.

Equations

• Lake.CacheRef.get? inputHash cache = ST.Ref.modifyGet cache fun (m : Lake.CacheMap) => (Lake.CacheMap.get? inputHash m, m)

@[inline]

def Lake.CacheRef.insert {α : Type u_1} [Lean.ToJson α] (inputHash : Hash) (val : α) (cache : CacheRef) : BaseIO Unit

Associate output data with the given the input hash.

Equations

• Lake.CacheRef.insert inputHash val cache = ST.Ref.modify cache fun (x : Lake.CacheMap) => Lake.CacheMap.insert inputHash (Lean.toJson val) x

Local Cache

structure Lake.Cache : Type

The Lake cache directory.

• dir : System.FilePath

def Lake.instInhabitedCache.default : Cache

Equations

• Lake.instInhabitedCache.default = { dir := default }

instance Lake.instInhabitedCache : Inhabited Cache

Equations

• Lake.instInhabitedCache = { default := Lake.instInhabitedCache.default }

@[inline]

def Lake.Cache.artifactDir (cache : Cache) : System.FilePath

Returns the artifact directory for the Lake cache.

Equations

• cache.artifactDir = cache.dir / { toString := "artifacts" }

@[inline]

def Lake.Cache.artifactPath (cache : Cache) (contentHash : Hash) (ext : String := "art") : System.FilePath

Returns the path to artifact in the Lake cache with extension ext.

Equations

• cache.artifactPath contentHash ext = cache.artifactDir / Lake.artifactPath contentHash ext

def Lake.Cache.getArtifact? (cache : Cache) (descr : ArtifactDescr) : BaseIO (Option Artifact)

Returns the artifact in the Lake cache corresponding the given artifact description.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Cache.getArtifact (cache : Cache) (descr : ArtifactDescr) : EIO String Artifact

Returns the artifact in the Lake cache corresponding the given artifact description. Errors if missing.

Equations

• One or more equations did not get rendered due to their size.

def Lake.Cache.getArtifactPaths (cache : Cache) (descrs : Array ArtifactDescr) : LogIO (Vector System.FilePath descrs.size)

Returns path to the artifact for each output. Errors if any are missing.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Cache.outputsDir (cache : Cache) : System.FilePath

The directory where input-to-output mappings are stored in the Lake cache.

Equations

• cache.outputsDir = cache.dir / { toString := "outputs" }

@[inline]

def Lake.Cache.outputsFile (cache : Cache) (scope : String) (inputHash : Hash) : System.FilePath

The file containing the outputs of the the given input for the package.

Equations

• cache.outputsFile scope inputHash = cache.outputsDir / { toString := scope } / { toString := toString inputHash ++ toString ".json" }

def Lake.Cache.writeOutputsCore (cache : Cache) (scope : String) (inputHash : Hash) (outputs : Lean.Json) : IO Unit

Cache the outputs corresponding to the given input for the package.

Equations

• cache.writeOutputsCore scope inputHash outputs = do Lake.createParentDirs (cache.outputsFile scope inputHash) IO.FS.writeFile (cache.outputsFile scope inputHash) outputs.compress

@[inline]

def Lake.Cache.writeOutputs {α : Type u_1} [Lean.ToJson α] (cache : Cache) (scope : String) (inputHash : Hash) (outputs : α) : IO Unit

Cache the outputs corresponding to the given input for the package.

Equations

• cache.writeOutputs scope inputHash outputs = cache.writeOutputsCore scope inputHash (Lean.toJson outputs)

def Lake.Cache.writeMap (cache : Cache) (scope : String) (map : CacheMap) : IO Unit

Cache the input-to-outputs mappings from a CacheMap.

Equations

• cache.writeMap scope map = Std.HashMap.forM (fun (i : Lake.Hash) (o : Lean.Json) => cache.writeOutputsCore scope i o) map

def Lake.Cache.readOutputs? (cache : Cache) (scope : String) (inputHash : Hash) : LogIO (Option Lean.Json)

Retrieve the cached outputs corresponding to the given input for the package (if any).

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.Cache.revisionDir (cache : Cache) : System.FilePath

The directory where input-to-output mappings of downloaded package revisions are cached.

Equations

• cache.revisionDir = cache.dir / { toString := "revisions" }

@[inline]

def Lake.Cache.revisionPath (cache : Cache) (scope rev : String) : System.FilePath

Returns path to the input-to-output mappings of a downloaded package revision.

Equations

• cache.revisionPath scope rev = cache.revisionDir / { toString := scope } / { toString := toString rev ++ toString ".jsonl" }

Remote Cache Service

structure Lake.CacheService : Type

Configuration of a remote cache service (e.g., Reservoir or an S3 bucket).

A given configuration is not required to support all cache service functions, and no validation of the configuration is performed by its operations. Users should construct a service that supports the desired functions by using CacheService's smart constructors (e.g., reservoir, uploadService).

• key : String
• artifactEndpoint : String
• revisionEndpoint : String
• isReservoir : Bool

  Is this a Reservoir cache service configuration?

• apiEndpoint : String
• repoScope : Bool

Constructors

@[inline]

def Lake.CacheService.reservoirService (apiEndpoint : String) (repoScope : Bool := false) : CacheService

Constructs a CacheService for a Reservoir endpoint.

Equations

• Lake.CacheService.reservoirService apiEndpoint repoScope = { isReservoir := true, apiEndpoint := apiEndpoint, repoScope := repoScope }

@[inline]

def Lake.CacheService.uploadService (key artifactEndpoint revisionEndpoint : String) : CacheService

Constructs a CacheService to upload artifacts and/or outputs to an S3 endpoint.

Equations

• Lake.CacheService.uploadService key artifactEndpoint revisionEndpoint = { key := key, artifactEndpoint := artifactEndpoint, revisionEndpoint := revisionEndpoint }

@[inline]

def Lake.CacheService.downloadService (artifactEndpoint revisionEndpoint : String) : CacheService

Constructs a CacheService to download artifacts and/or outputs from to an S3 endpoint.

Equations

• Lake.CacheService.downloadService artifactEndpoint revisionEndpoint = { artifactEndpoint := artifactEndpoint, revisionEndpoint := revisionEndpoint }

@[inline]

def Lake.CacheService.downloadArtsService (artifactEndpoint : String) : CacheService

Constructs a CacheService to download just artifacts from to an S3 endpoint.

Equations

• Lake.CacheService.downloadArtsService artifactEndpoint = { artifactEndpoint := artifactEndpoint }

@[inline]

def Lake.CacheService.withRepoScope (service : CacheService) (repoScope : Bool := true) : CacheService

Reconfigures the cache service to interpret scopes as repositories (or not if false).

For custom endpoints, if true, Lake wil augment the provided scope with toolchain and platform information in a manner similar to Reservoir.

Equations

• One or more equations did not get rendered due to their size.

Artifact Transfer

def Lake.CacheService.artifactContentType : String

The MIME type of Lake/Reservoir artifact.

Equations

• Lake.CacheService.artifactContentType = "application/vnd.reservoir.artifact"

def Lake.CacheService.artifactUrl (contentHash : Hash) (service : CacheService) (scope : String) : String

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.downloadArtifact (descr : ArtifactDescr) (cache : Cache) (service : CacheService) (scope : String) (force : Bool := false) : LoggerIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.downloadArtifacts (descrs : Array ArtifactDescr) (cache : Cache) (service : CacheService) (scope : String) (force : Bool := false) : LoggerIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.downloadOutputArtifacts (map : CacheMap) (cache : Cache) (service : CacheService) (localScope remoteScope : String) (force : Bool := false) : LoggerIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.uploadArtifact (contentHash : Hash) (art : System.FilePath) (service : CacheService) (scope : String) : LoggerIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.uploadArtifacts {n : Nat} (descrs : Vector ArtifactDescr n) (paths : Vector System.FilePath n) (service : CacheService) (scope : String) : LoggerIO Unit

Equations

• Lake.CacheService.uploadArtifacts descrs paths service scope = n.forM fun (n_1 : Nat) (h : n_1 < n) => Lake.CacheService.uploadArtifact descrs[n_1].hash paths[n_1] service scope

Output Transfer

def Lake.CacheService.mapContentType : String

The MIME type of Lake/Reservoir input-to-output mappings for a Git revision.

Equations

• Lake.CacheService.mapContentType = "application/vnd.reservoir.outputs+json-lines"

def Lake.CacheService.revisionUrl (rev : String) (service : CacheService) (scope : String) (platform toolchain : String := "") : String

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.downloadRevisionOutputs? (rev : String) (cache : Cache) (service : CacheService) (localScope remoteScope : String) (platform toolchain : String := "") (force : Bool := false) : LoggerIO (Option CacheMap)

Equations

• One or more equations did not get rendered due to their size.

def Lake.CacheService.uploadRevisionOutputs (rev : String) (outputs : System.FilePath) (service : CacheService) (scope : String) (platform toolchain : String := "") : LoggerIO Unit

Equations

• One or more equations did not get rendered due to their size.