@[inline]

def Lake.artifactPath (contentHash : Hash) (ext : String := "art") : System.FilePath

Returns the relative file path used for an artifact in the Lake cache (i.e., {hash}.{ext}).

Equations

• Lake.artifactPath contentHash ext = if ext.isEmpty = true then { toString := contentHash.toString } else { toString := toString contentHash ++ toString "." ++ toString ext }

structure Lake.ArtifactDescr : Type

The information needed to identify a single artifact within the Lake cache.

• hash : Hash

  The artifact's content hash.

• ext : String

  The artifact's file extension.

instance Lake.instInhabitedArtifactDescr : Inhabited ArtifactDescr

Equations

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

def Lake.instInhabitedArtifactDescr.default : ArtifactDescr

Equations

• Lake.instInhabitedArtifactDescr.default = { hash := default, ext := default }

def Lake.instReprArtifactDescr.repr : ArtifactDescr → Nat → Std.Format

Equations

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

instance Lake.instReprArtifactDescr : Repr ArtifactDescr

Equations

• Lake.instReprArtifactDescr = { reprPrec := Lake.instReprArtifactDescr.repr }

@[inline]

def Lake.artifactWithExt (contentHash : Hash) (ext : String := "art") : ArtifactDescr

A content-hashed artifact that should have the file extension ext.

Many applications care about the extension of a file (e.g., use it determine what kind of operation to perform), so the content hash alone may not be sufficient to produce a useable artifact for consumers.

Equations

• Lake.artifactWithExt contentHash ext = { hash := contentHash, ext := ext }

@[inline]

def Lake.ArtifactDescr.relPath (self : ArtifactDescr) : System.FilePath

Returns the relative file path used for the output's artifact in the Lake cache (c.f. artifactPath).

Equations

• self.relPath = Lake.artifactPath self.hash self.ext

instance Lake.ArtifactDescr.instToString : ToString ArtifactDescr

Equations

• Lake.ArtifactDescr.instToString = { toString := fun (x : Lake.ArtifactDescr) => x.relPath.toString }

instance Lake.ArtifactDescr.instToJson : Lean.ToJson ArtifactDescr

Equations

• Lake.ArtifactDescr.instToJson = { toJson := fun (x : Lake.ArtifactDescr) => Lean.toJson x.relPath }

def Lake.ArtifactDescr.ofFilePath? (path : System.FilePath) : Except String ArtifactDescr

Parse an output's relative file path into an ArtifactDescr.

Equations

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

def Lake.ArtifactDescr.fromJson? (data : Lean.Json) : Except String ArtifactDescr

Equations

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

instance Lake.ArtifactDescr.instFromJson : Lean.FromJson ArtifactDescr

Equations

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

structure Lake.Artifactextends Lake.ArtifactDescr : Type

A file with a known content hash.

• hash : Hash
• ext : String
• path : System.FilePath

  The preferred path to the artifact on the file system.

• name : String

  The artifact's. This is used, for example, as a caption in traces.

• mtime : MTime

  The artifact's modification time (or 0 if unknown).

def Lake.instInhabitedArtifact.default : Artifact

Equations

• Lake.instInhabitedArtifact.default = { descr := default, path := default, name := default, mtime := default }

instance Lake.instInhabitedArtifact : Inhabited Artifact

Equations

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

def Lake.instReprArtifact.repr : Artifact → Nat → Std.Format

Equations

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

instance Lake.instReprArtifact : Repr Artifact

Equations

• Lake.instReprArtifact = { reprPrec := Lake.instReprArtifact.repr }

@[inline]

def Lake.Artifact.withName (name : String) (self : Artifact) : Artifact

Sets the name of the artifact.

Equations

• Lake.Artifact.withName name self = { descr := self.descr, path := self.path, name := name, mtime := self.mtime }

@[inline]

def Lake.Artifact.useLocalFile (path : System.FilePath) (self : Artifact) : Artifact

Sets the name and path of the artifact using the file outside the Lake artifact cache.

Equations

• Lake.Artifact.useLocalFile path self = { descr := self.descr, path := path, mtime := self.mtime }

def Lake.Artifact.trace (self : Artifact) : BuildTrace

The build trace formed from this single artifact.

Equations

• self.trace = { caption := self.name, hash := self.hash, mtime := self.mtime }