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

Instances For

source
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.

Instances For

source
instance Lake.instInhabitedArtifactDescr :
Inhabited ArtifactDescr
Equations

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

source
def Lake.instInhabitedArtifactDescr.default :
ArtifactDescr
Equations

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

Instances For

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

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

Instances For

source
instance Lake.instReprArtifactDescr :
Repr ArtifactDescr
Equations

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

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

Instances For

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

Instances For

source
instance Lake.ArtifactDescr.instToString :
ToString ArtifactDescr
Equations

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

source
instance Lake.ArtifactDescr.instToJson :
Lean.ToJson ArtifactDescr
Equations

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

source
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.

Instances For

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

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

Instances For

source
instance Lake.ArtifactDescr.instFromJson :
Lean.FromJson ArtifactDescr
Equations

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

source
structure Lake.Artifact extends 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).

Instances For

source
def Lake.instInhabitedArtifact.default :
Artifact
Equations

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

Instances For

source
instance Lake.instInhabitedArtifact :
Inhabited Artifact
Equations

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

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

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

Instances For

source
instance Lake.instReprArtifact :
Repr Artifact
Equations

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

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

Instances For

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

Instances For

source
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 }

Instances For