structure Lake.Artifact : Type

A file with a known content hash.

• path : System.FilePath

  The path to the artifact on the file system.

• name : String

  The name of the artifact. This is used, for example, as a caption in traces.

• mtime : MTime

  The modification time of the artifact (or 0 if unknown).

• hash : Hash

  The content hash of the artifact.

def Lake.instInhabitedArtifact.default : Artifact

Equations

• Lake.instInhabitedArtifact.default = { path := default, name := default, mtime := default, hash := 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 = { path := self.path, name := name, mtime := self.mtime, hash := self.hash }

@[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 = { path := path, mtime := self.mtime, hash := self.hash }

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 }