structure Lake.Cache : Type

The Lake cache directory.

• dir : System.FilePath

instance Lake.instInhabitedCache : Inhabited Cache

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

Returns whether the Lake cache is disabled.

An empty directory string indicates the cache is disabled.

@[inline]

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

Returns the artifact directory for the Lake cache.

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

@[inline]

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

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

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

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

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

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

Load a CacheMap from a JSON Lines file.

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.

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.

@[reducible, inline]

abbrev Lake.CacheRef : Type

A mutable reference to a 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.

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