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.

def Lake.CacheMap.schemaVersion : String

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

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

Parse a Cache from a JSON Lines string.

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

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

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

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) : LogIO Unit

Write a CacheMap to a JSON Lines file.

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

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

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

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

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

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) : BaseIO Unit

Associate output data with the given the input hash.

Local Cache

structure Lake.Cache : Type

The Lake cache directory.

• dir : System.FilePath

def Lake.instInhabitedCache.default : Cache

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.

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

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

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.

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.

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

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.

@[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) : IO Unit

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

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

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

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.

@[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) : CacheService

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

@[inline]

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

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

@[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 will augment the provided scope with toolchain and platform information in a manner similar to Reservoir.

Artifact Transfer

def Lake.CacheService.artifactContentType : String

The MIME type of Lake/Reservoir artifact.

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

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

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

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

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

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

Output Transfer

def Lake.CacheService.mapContentType : String

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

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

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

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