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

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.

@[implicit_reducible]

instance Lake.instInhabitedArtifactDescr : Inhabited ArtifactDescr

def Lake.instInhabitedArtifactDescr.default : ArtifactDescr

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

@[implicit_reducible]

instance Lake.instReprArtifactDescr : Repr ArtifactDescr

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

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

@[implicit_reducible]

instance Lake.ArtifactDescr.instToString : ToString ArtifactDescr

@[implicit_reducible]

instance Lake.ArtifactDescr.instToJson : Lean.ToJson ArtifactDescr

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

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

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

@[implicit_reducible]

instance Lake.ArtifactDescr.instFromJson : Lean.FromJson ArtifactDescr

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

@[implicit_reducible]

instance Lake.instInhabitedArtifact : Inhabited Artifact

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

@[implicit_reducible]

instance Lake.instReprArtifact : Repr Artifact

@[inline]

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

Sets the name of the artifact.

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

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

The build trace formed from this single artifact.