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.

def Lake.CacheMap.schemaVersion : Date

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

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.

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.

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.

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.

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.

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

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

@[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.

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

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

Cache Ref

@[reducible, inline]

abbrev Lake.CacheRef : Type

A mutable reference to a CacheMap.

@[inline]

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

@[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.

@[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.

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

@[inline]

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

Constructs a service identifier from a user-provided name.

@[inline]

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

Returns the string representation of the service identifier.

@[implicit_reducible]

instance Lake.CacheServiceName.instToString : ToString CacheServiceName

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.

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

Constructs a service scope from a GitHub repository name.

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

Returns whether this is a repository scope.

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

Returns a string representation of the scope.

@[implicit_reducible]

instance Lake.CacheServiceScope.instToString : ToString CacheServiceScope

Cache Output

def Lake.CacheOutput.schemaVersion : String

The current version of the output file format.

structure Lake.CacheOutput : Type

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

@[implicit_reducible]

instance Lake.instInhabitedCacheOutput : Inhabited CacheOutput

def Lake.instInhabitedCacheOutput.default : CacheOutput

@[inline]

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

For internal use only.

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

@[implicit_reducible]

instance Lake.CacheOutput.instToJson : Lean.ToJson CacheOutput

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

@[implicit_reducible]

instance Lake.CacheOutput.instFromJson : Lean.FromJson CacheOutput

Local Cache

structure Lake.Cache : Type

The Lake cache directory.

• dir : System.FilePath

def Lake.instInhabitedCache.default : Cache

@[implicit_reducible]

instance Lake.instInhabitedCache : Inhabited Cache

@[inline]

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

Returns the artifact directory for the Lake cache.

@[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.

@[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.

@[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.

@[inline]

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

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

@[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.

@[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.

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.

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

@[inline]

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

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

@[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.

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.

@[inline]

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

Returns true if this platform identifier is the none indicator.

def Lake.CachePlatform.system : CachePlatform

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

@[inline]

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

Constructs a platform identifier from a user-provided string.

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

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

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

Returns a string representation of the platform identifier.

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.

@[inline]

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

Returns true if this toolchain identifier is the none indicator.

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

Constructs a toolchain identifier from a user-provided string.

@[inline]

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

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

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

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

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

Returns a string representation of the toolchain identifier.

Remote Cache Service

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

For internal use only.

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.

@[inline]

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

Returns whether this is a Reservoir cache service configuration.

Constructors

@[inline]

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

Constructs a CacheService for a Reservoir endpoint.

@[inline]

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

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

@[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.

@[inline]

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

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

@[inline]

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

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

Artifact Transfer

def Lake.CacheService.artifactContentType : String

The MIME type of a Lake/Reservoir artifact.

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

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

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

Multi-Artifact Transfer

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

@[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

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

Output Transfer

def Lake.CacheService.mapContentType : String

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

def Lake.CacheService.revisionUrl (rev : String) (service : CacheService) (scope : CacheServiceScope) (platform : CachePlatform := CachePlatform.none) (toolchain : CacheToolchain := CacheToolchain.none) : String

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)

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