Documentation

Lake.Build.Trace

Lake Traces #

This module defines Lake traces and associated utilities. Traces are used to determine whether a Lake build artifact is dirty (needs to be rebuilt) or is already up-to-date. The primary type is Lake.BuildTrace.

Utilities #

class Lake.CheckExists (i : Type u) :
  • checkExists : iBaseIO Bool

    Check whether there already exists an artifact for the given target info.

Instances

Trace Abstraction #

@[inline]
def Lake.computeTrace {α : Type u_1} {m : Type u_2 → Type u_3} {τ : Type u_2} {n : Type u_2 → Type u_4} [ComputeTrace α m τ] [MonadLiftT m n] (a : α) :
n τ

Compute the trace of an object in a supporting monad.

Equations
class Lake.NilTrace (α : Type u) :
  • nilTrace : α

    The nil trace. Should not unduly clash with a proper trace.

Instances
class Lake.MixTrace (α : Type u) :
  • mixTrace : ααα

    Combine two traces. The result should be dirty if either of the inputs is dirty.

Instances
def Lake.mixTraceList {τ : Type u_1} [MixTrace τ] [NilTrace τ] (traces : List τ) :
τ
Equations
def Lake.mixTraceArray {τ : Type u_1} [MixTrace τ] [NilTrace τ] (traces : Array τ) :
τ
Equations
@[inline]
def Lake.computeListTrace {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (as : List α) :
n τ
Equations
instance Lake.instComputeTraceListOfMonad {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] [Monad m] :
ComputeTrace (List α) m τ
Equations
@[inline]
def Lake.computeArrayTrace {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (as : Array α) :
n τ
Equations
instance Lake.instComputeTraceArrayOfMonad {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] [Monad m] :
Equations

Hash Trace #

@[inline]
Equations
Equations
@[inline]
def Lake.Hash.mix (h1 h2 : Hash) :
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
def Lake.pureHash {α : Type u_1} [ComputeHash α Id] (a : α) :

Compute the hash of object a in a pure context.

Equations
@[inline]
def Lake.computeHash {α : Type u_1} {m : TypeType u_2} {n : TypeType u_3} [ComputeHash α m] [MonadLiftT m n] (a : α) :

Compute the hash an object in an supporting monad.

Equations

Compute the hash of a binary file. Binary files are equivalent only if they are byte identical.

Equations

Compute the hash of a text file. Normalizes \r\n sequences to \n for cross-platform compatibility.

Equations

A wrapper around FilePath that adjusts its ComputeHash implementation to normalize \r\n sequences to \n for cross-platform compatibility.

Instances For
@[inline]

Compute the hash of a file. If text := true, normalize line endings.

Equations
@[inline]
def Lake.computeArrayHash {α : Type u_1} {m : TypeType u_2} [ComputeHash α m] [Monad m] (as : Array α) :

Compute the hash of each element of an array and combine them (left-to-right).

Equations

Modification Time (MTime) Trace #

Equations
class Lake.GetMTime (α : Type u) :
  • getMTime : αIO MTime

    Return the modification time of an object.

Instances
@[inline]

Return the modification time of a file recorded by the OS.

Equations
@[specialize #[]]
def Lake.MTime.checkUpToDate {i : Type u_1} [GetMTime i] (info : i) (self : MTime) :

Check if info is up-to-date using modification time. That is, check if the info is newer than self.

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

Lake Build Trace #

@[inline]
Equations
@[inline]
Equations
@[specialize #[]]
def Lake.BuildTrace.compute {α : Type u_1} {m : TypeType u_2} [ComputeHash α m] [MonadLiftT m IO] [GetMTime α] (info : α) :
Equations
Equations
@[specialize #[]]
def Lake.BuildTrace.checkAgainstHash {i : Type u_1} [CheckExists i] (info : i) (hash : Hash) (self : BuildTrace) :

Check if the info is up-to-date using a hash. That is, check that info exists and its input hash matches this trace's hash.

Equations
@[inline]
def Lake.BuildTrace.checkAgainstTime {i : Type u_1} [GetMTime i] (info : i) (self : BuildTrace) :

Check if the info is up-to-date using modification time. That is, check if the info is newer than this input trace's modification time.

Equations
@[specialize #[], deprecated "Should not be done manually, but as part of `buildUnlessUpToDate`." (since := "2024-06-14")]
def Lake.BuildTrace.checkAgainstFile {i : Type u_1} [CheckExists i] [GetMTime i] (info : i) (traceFile : System.FilePath) (self : BuildTrace) :

Check if the info is up-to-date using a trace file. If the file exists, match its hash to this trace's hash. If not, check if the info is newer than this trace's modification time.

Deprecated: Should not be done manually, but as part of buildUnlessUpToDate.

Equations
  • One or more equations did not get rendered due to their size.
@[deprecated "Should not be done manually, but as part of `buildUnlessUpToDate`." (since := "2024-06-14")]

Write trace to a file.

Deprecated: Should not be done manually, but as part of buildUnlessUpToDate.

Equations