Cache Map

structure Lake.CacheMap.Entry : Type

• out : Lean.Json
• platformIndependent : Bool

@[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 Lake.CacheMap.Entry

def Lake.CacheMap.schemaVersion : Date

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

Equations

• Lake.CacheMap.schemaVersion = { year := 2026, month := 3, day := 17 }

def Lake.CacheMap.parse (inputName contents : String) (platformIndependent : Bool := false) : LoggerIO CacheMap

Parse a Cache from a JSON Lines string.

If platformIndependent := true, all mappings within the file are considered platform-independent. Otherwise, they are considered platform-dependent.

Equations

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

def Lake.CacheMap.load (file : System.FilePath) (platformIndependent : Bool := false) : LogIO CacheMap

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

If platformIndependent := true, all mappings within the file are considered platform-independent. Otherwise, they are considered platform-dependent.

Equations

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

def Lake.CacheMap.load? (file : System.FilePath) (platformIndependent : Bool := false) : LogIO (Option CacheMap)

Loads a CacheMap from a JSON Lines file. Returns none if the file does not exist. Errors if the manifest is ill-formatted or the read fails for other reasons.

If platformIndependent := true, all mappings within the file are considered platform-independent. Otherwise, they are considered platform-dependent.

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) (platformIndependent : Bool := false) : LogIO Unit

Write a CacheMap to a JSON Lines file.

If platformIndependent := true, platform-dependent mappings within the map will not be written to the 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 = do let x ← Std.HashMap.get? cache inputHash some x.out

@[inline]

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

Associate output data with the given the input hash.

Equations

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

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) (platformIndependent : Bool := false) : BaseIO Unit

Associate output data with the given the input hash.

Equations

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

Cache Service Name

structure Lake.CacheServiceName : Type

The type of service identifiers used by the Lake ache.

• raw : String

def Lake.CacheServiceName.reservoir : CacheServiceName

The identifier used for the default Reservoir service (i.e., reservoir).

Equations

• Lake.CacheServiceName.reservoir = { raw := "reservoir" }

@[inline]

def Lake.CacheServiceName.ofString (s : String) : CacheServiceName

Constructs a service identifier from a user-provided name.

Equations

• Lake.CacheServiceName.ofString s = { raw := s }

@[inline]

def Lake.CacheServiceName.toString (self : CacheServiceName) : String

Returns the string representation of the service identifier.

Equations

• self.toString = Lake.CacheServiceName.raw✝ self

@[implicit_reducible]

instance Lake.CacheServiceName.instToString : ToString CacheServiceName

Equations

• Lake.CacheServiceName.instToString = { toString := Lake.CacheServiceName.toString }

Cache Service Scope

structure Lake.CacheServiceScope : Type

The type of artifact prefixes in a Lake cache service.

• impl : CacheServiceScopeImpl

def Lake.CacheServiceScope.ofString (s : String) : CacheServiceScope

Constructs a generic service scope from a user-provided string.

Equations

• Lake.CacheServiceScope.ofString s = { impl := Lake.CacheServiceScopeImpl.str✝ s }

def Lake.CacheServiceScope.ofRepo (fullName : String) : CacheServiceScope

Constructs a service scope from a GitHub repository name.

Equations

• Lake.CacheServiceScope.ofRepo fullName = { impl := Lake.CacheServiceScopeImpl.repo✝ fullName }

def Lake.CacheServiceScope.isRepo (self : CacheServiceScope) : Bool

Returns whether this is a repository scope.

Equations

• self.isRepo = match Lake.CacheServiceScope.impl✝ self with | Lake.CacheServiceScopeImpl.repo✝ s => true | x => false

def Lake.CacheServiceScope.toString (self : CacheServiceScope) : String

Returns a string representation of the scope.

Equations

• self.toString = match Lake.CacheServiceScope.impl✝ self with | Lake.CacheServiceScopeImpl.str✝ s => s | Lake.CacheServiceScopeImpl.repo✝ s => s

@[implicit_reducible]

instance Lake.CacheServiceScope.instToString : ToString CacheServiceScope

Equations

• Lake.CacheServiceScope.instToString = { toString := Lake.CacheServiceScope.toString }

Cache Output

def Lake.CacheOutput.schemaVersion : String

The current version of the output file format.

Equations

• Lake.CacheOutput.schemaVersion = "2026-02-25"

structure Lake.CacheOutput : Type

• data : Lean.Json
• service? : Option CacheServiceName
• scope? : Option CacheServiceScope

@[implicit_reducible]

instance Lake.instInhabitedCacheOutput : Inhabited CacheOutput

Equations

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

def Lake.instInhabitedCacheOutput.default : CacheOutput

Equations

• Lake.instInhabitedCacheOutput.default = { data := default, service? := default, scope? := default }

@[inline]

def Lake.CacheOutput.ofData (data : Lean.Json) : CacheOutput

For internal use only.

Equations

• Lake.CacheOutput.ofData data = { data := data }

def Lake.CacheOutput.toJson (out : CacheOutput) : Lean.Json

Equations

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

@[implicit_reducible]

instance Lake.CacheOutput.instToJson : Lean.ToJson CacheOutput

Equations

• Lake.CacheOutput.instToJson = { toJson := Lake.CacheOutput.toJson }

def Lake.CacheOutput.fromJson? (json : Lean.Json) : Except String CacheOutput

Equations

• One or more equations did not get rendered due to their size.
• Lake.CacheOutput.fromJson? json = (fun (__r : Unit) => pure (Lake.CacheOutput.ofData json)) PUnit.unit

@[implicit_reducible]

instance Lake.CacheOutput.instFromJson : Lean.FromJson CacheOutput

Equations

• Lake.CacheOutput.instFromJson = { fromJson? := Lake.CacheOutput.fromJson? }

Local Cache

structure Lake.Cache : Type

The Lake cache directory.

• dir : System.FilePath

def Lake.instInhabitedCache.default : Cache

Equations

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

@[implicit_reducible]

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

@[deprecated "Deprecated without replacelement." (since := "2025-03-04")]

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.

@[deprecated "Deprecated without replacelement." (since := "2025-03-04")]

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.

@[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 given input for the package.

Equations

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

@[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 = Lake.Cache.writeOutputsCore✝ cache scope inputHash (Lean.toJson outputs) none none

def Lake.Cache.writeMap (cache : Cache) (scope : String) (map : CacheMap) (service? : Option CacheServiceName := none) (remoteScope? : Option CacheServiceScope := none) : IO Unit

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

Equations

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

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

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" }

Cache Platform

structure Lake.CachePlatform : Type

The type of platform identifiers used by the Lake ache.

• raw : String

def Lake.CachePlatform.none : CachePlatform

An indicator that no platform should be included in a cache scope.

Equations

• Lake.CachePlatform.none = { raw := "" }

@[inline]

def Lake.CachePlatform.isNone (self : CachePlatform) : Bool

Returns true if this platform identifier is the none indicator.

Equations

• self.isNone = (Lake.CachePlatform.raw✝ self).isEmpty

def Lake.CachePlatform.system : CachePlatform

The identifier of the host platform (e.g., System.Platform.target).

Equations

• Lake.CachePlatform.system = { raw := System.Platform.target }

@[inline]

def Lake.CachePlatform.ofString (s : String) : CachePlatform

Constructs a platform identifier from a user-provided string.

Equations

• Lake.CachePlatform.ofString s = { raw := s }

def Lake.CachePlatform.length (self : CachePlatform) : Nat

Returns the length of the platform identifier in Unicode code points.

Equations

• self.length = (Lake.CachePlatform.raw✝ self).length

def Lake.CachePlatform.toString (self : CachePlatform) : String

Returns a string representation of the platform identifier.

Equations

• self.toString = if self.isNone = true then "none" else Lake.CachePlatform.raw✝ self

Cache Toolchain

structure Lake.CacheToolchain : Type

The type of toolchain identifiers used by the Lake ache.

• raw : String

def Lake.CacheToolchain.none : CacheToolchain

An indicator that no toolchain should be included in a cache scope.

Equations

• Lake.CacheToolchain.none = { raw := "" }

@[inline]

def Lake.CacheToolchain.isNone (self : CacheToolchain) : Bool

Returns true if this toolchain identifier is the none indicator.

Equations

• self.isNone = (Lake.CacheToolchain.raw✝ self).isEmpty

def Lake.CacheToolchain.ofString (s : String) : CacheToolchain

Constructs a toolchain identifier from a user-provided string.

Equations

• Lake.CacheToolchain.ofString s = { raw := Lake.normalizeToolchain s }

@[inline]

def Lake.CacheToolchain.ofElanToolchain (s : String) : CacheToolchain

For internal use only. See Lake.Env.cacheToolchain.

Equations

• Lake.CacheToolchain.ofElanToolchain s = { raw := s }

def Lake.CacheToolchain.length (self : CacheToolchain) : Nat

Returns the length of the toolchain identifier in Unicode code points.

Equations

• self.length = (Lake.CacheToolchain.raw✝ self).length

def Lake.CacheToolchain.toString (self : CacheToolchain) : String

Returns a string representation of the toolchain identifier.

Equations

• self.toString = if self.isNone = true then "none" else Lake.CacheToolchain.raw✝ self

Remote Cache Service

def Lake.downloadArtifactCore (hash : Hash) (url : String) (path : System.FilePath) : LogIO Unit

For internal use only.

Equations

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

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).

• impl : CacheServiceImpl

instance Lake.instNonemptyCacheService : Nonempty CacheService

@[inline]

def Lake.CacheService.name? (service : CacheService) : Option CacheServiceName

Returns the name (if any) used to identify the service.

Equations

• service.name? = Lake.CacheServiceImpl.name?✝ (Lake.CacheService.impl✝ service)

@[inline]

def Lake.CacheService.isReservoir (service : CacheService) : Bool

Returns whether this is a Reservoir cache service configuration.

Equations

• service.isReservoir = Lake.CacheServiceImpl.isReservoir✝ (Lake.CacheService.impl✝ service)

Constructors

@[inline]

def Lake.CacheService.reservoirService (apiEndpoint : String) (name? : Option CacheServiceName := some CacheServiceName.reservoir) : CacheService

Constructs a CacheService for a Reservoir endpoint.

Equations

• Lake.CacheService.reservoirService apiEndpoint name? = { impl := { name? := name?, isReservoir := true, apiEndpoint := apiEndpoint } }

@[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 = { impl := { key := key, artifactEndpoint := artifactEndpoint, revisionEndpoint := revisionEndpoint } }

@[inline]

def Lake.CacheService.downloadService (artifactEndpoint revisionEndpoint : String) (name? : Option CacheServiceName := none) : CacheService

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

Equations

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

@[inline]

def Lake.CacheService.downloadArtsService (artifactEndpoint : String) (name? : Option CacheServiceName := none) : CacheService

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

Equations

• Lake.CacheService.downloadArtsService artifactEndpoint name? = { impl := { name? := name?, artifactEndpoint := artifactEndpoint } }

@[inline]

def Lake.CacheService.withKey (service : CacheService) (key : String) : CacheService

Reconfigures the cache service to use the provided key (for uploads).

Equations

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

Artifact Transfer

def Lake.CacheService.artifactContentType : String

The MIME type of a Lake/Reservoir artifact.

Equations

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

def Lake.CacheService.artifactUrl (contentHash : Hash) (service : CacheService) (scope : CacheServiceScope) : 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 : CacheServiceScope) (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 : CacheServiceScope) : LoggerIO Unit

Equations

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

Multi-Artifact Transfer

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

Equations

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

@[deprecated "Deprecated without replacement." (since := "2026-02-27")]

def Lake.CacheService.downloadOutputArtifacts (map : CacheMap) (cache : Cache) (service : CacheService) (localScope : String) (remoteScope : CacheServiceScope) (force : Bool := false) : 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 : CacheServiceScope) : LoggerIO Unit

Equations

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

Output Transfer

def Lake.CacheService.mapContentType : String

The MIME type of a 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 : CacheServiceScope) (platform : CachePlatform := CachePlatform.none) (toolchain : CacheToolchain := CacheToolchain.none) : 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 : String) (remoteScope : CacheServiceScope) (platform : CachePlatform := CachePlatform.none) (toolchain : CacheToolchain := CacheToolchain.none) (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 : CacheServiceScope) (platform : CachePlatform := CachePlatform.none) (toolchain : CacheToolchain := CacheToolchain.none) : LoggerIO Unit

Equations

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