structure Lake.Cache : Type

The Lake cache directory.

• dir : System.FilePath

instance Lake.instInhabitedCache : Inhabited Cache

Equations

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

def Lake.Cache.isDisabled (cache : Cache) : Bool

Returns whether the Lake cache is disabled.

An empty directory string indicates the cache is disabled.

Equations

• cache.isDisabled = cache.dir.toString.isEmpty

@[inline]

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

Returns the artifact directory for the Lake cache.

Equations

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

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

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

def Lake.Cache.getArtifact? (cache : Cache) (contentHash : Hash) (ext : String := "art") : BaseIO (Option Artifact)

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

If the Lake cache is disabled, the behavior of this function is undefined.

Equations

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

@[inline]

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

The file where the package's input mapping is stored in the Lake cache.

Equations

• cache.inputsDir = cache.dir / { toString := "inputs" }

def Lake.Cache.inputsFile (pkgName : String) (cache : Cache) : System.FilePath

The file where a package's input mapping is stored in the Lake cache.

Equations

• Lake.Cache.inputsFile pkgName cache = cache.inputsDir / { toString := toString "" ++ toString pkgName ++ toString ".jsonl" }

@[reducible, inline]

abbrev Lake.CacheMap : Type

Maps an input hash to a structure of 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.load (inputsFile : System.FilePath) : LogIO CacheMap

Load a CacheMap from a JSON Lines file.

Equations

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

def Lake.CacheMap.save (inputsFile : 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.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

@[reducible, inline]

abbrev Lake.CacheRef : Type

A mutable reference to a CacheMap.

Equations

• Lake.CacheRef = IO.Ref Lake.CacheMap

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