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) : Type u

• checkExists : i → BaseIO Bool

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

@[implicit_reducible]

instance Lake.instCheckExistsFilePath : CheckExists System.FilePath

Trace Abstraction

class Lake.ComputeTrace (α : Type u) (m : outParam (Type v → Type w)) (τ : Type v) : Type (max u w)

• computeTrace : α → m τ

  Compute the trace of an object in its preferred monad.

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

class Lake.NilTrace (α : Type u) : Type u

• nilTrace : α

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

@[implicit_reducible]

instance Lake.inhabitedOfNilTrace {α : Type u_1} [NilTrace α] : Inhabited α

class Lake.MixTrace (α : Type u) : Type u

• mixTrace : α → α → α

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

def Lake.mixTraceList {τ : Type u_1} [MixTrace τ] [NilTrace τ] (traces : List τ) : τ

def Lake.mixTraceArray {τ : Type u_1} [MixTrace τ] [NilTrace τ] (traces : Array τ) : τ

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

@[implicit_reducible]

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 τ

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

@[implicit_reducible]

instance Lake.instComputeTraceArrayOfMonad {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] [Monad m] : ComputeTrace (Array α) m τ

Hash Trace

structure Lake.Hash : Type

A content hash.

• val : UInt64

def Lake.instReprHash.repr : Hash → Nat → Std.Format

@[implicit_reducible]

instance Lake.instReprHash : Repr Hash

def Lake.instDecidableEqHash.decEq (x✝ x✝¹ : Hash) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Lake.instDecidableEqHash : DecidableEq Hash

@[implicit_reducible]

instance Lake.Hash.instHashable : Hashable Hash

def Lake.Hash.nil : Hash

@[implicit_reducible]

instance Lake.Hash.instNilTrace : NilTrace Hash

@[inline]

def Lake.Hash.ofNat (n : Nat) : Hash

Constructs a hash with with the value n. This is not equivalent to the hash of n.

def Lake.Hash.ofJsonNumber? (n : Lean.JsonNumber) : Except String Hash

Parse a hash from a JSON number.

def Lake.Hash.ofHex (s : String) : Hash

Parse a hash from a string of hexadecimal digits. Does no validation.

def Lake.Hash.ofHex? (s : String) : Option Hash

Parse a hash from a 16-digit string of hexadecimal digits.

def Lake.Hash.hex (self : Hash) : String

Returns the hash as 16-digit lowercase hex string.

def Lake.Hash.ofDecimal? (s : String) : Option Hash

Parse a hash from a string of decimal digits.

@[inline]

def Lake.Hash.ofString? (s : String) : Option Hash

def Lake.Hash.load? (hashFile : System.FilePath) : BaseIO (Option Hash)

Laod a hash from a .hash file.

@[inline]

def Lake.Hash.mix (h1 h2 : Hash) : Hash

@[implicit_reducible]

instance Lake.Hash.instMixTrace : MixTrace Hash

@[inline]

def Lake.Hash.toString (self : Hash) : String

@[implicit_reducible]

instance Lake.Hash.instToString : ToString Hash

@[inline]

def Lake.Hash.ofHashable {α : Sort u_1} [Hashable α] (a : α) : Hash

Hash of a value using its Hashable instance.

@[inline]

def Lake.Hash.ofString (str : String) : Hash

Hash of a string (without line-ending normalization).

@[inline]

def Lake.Hash.ofText (str : String) : Hash

Hash of a line-ending normalized string.

@[inline]

def Lake.Hash.ofByteArray (bytes : ByteArray) : Hash

Hash of a sequence of bytes.

@[inline, deprecated Lake.Hash.ofHashable (since := "2026-02-06")]

def Lake.Hash.ofBool (b : Bool) : Hash

@[inline]

def Lake.Hash.toJson (self : Hash) : Lean.Json

@[implicit_reducible]

instance Lake.Hash.instToJson : Lean.ToJson Hash

def Lake.Hash.fromJson? (json : Lean.Json) : Except String Hash

@[implicit_reducible]

instance Lake.Hash.instFromJson : Lean.FromJson Hash

class Lake.ComputeHash (α : Type u) (m : outParam (Type → Type v)) : Type (max u v)

• computeHash : α → m Hash

  Compute the hash of an object in its preferred monad.

@[implicit_reducible]

instance Lake.instComputeTraceHashOfComputeHash {α : Type u_1} {m : Type → Type u_2} [ComputeHash α m] : ComputeTrace α m Hash

@[inline]

def Lake.pureHash {α : Type u_1} [ComputeHash α Id] (a : α) : Hash

Compute the hash of object a in a pure context.

@[inline]

def Lake.computeHash {α : Type u_1} {m : Type → Type u_2} {n : Type → Type u_3} [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash

Compute the hash an object in an supporting monad.

@[implicit_reducible]

instance Lake.instComputeHashIdOfHashable {α : Type u_1} [Hashable α] : ComputeHash α Id

def Lake.computeBinFileHash (file : System.FilePath) : IO Hash

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

@[implicit_reducible]

instance Lake.instComputeHashFilePathIO : ComputeHash System.FilePath IO

def Lake.computeTextFileHash (file : System.FilePath) : IO Hash

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

structure Lake.TextFilePath : Type

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

• path : System.FilePath

@[implicit_reducible]

instance Lake.instCoeTextFilePathFilePath : Coe TextFilePath System.FilePath

@[implicit_reducible]

instance Lake.instComputeHashTextFilePathIO : ComputeHash TextFilePath IO

@[implicit_reducible]

instance Lake.instToStringTextFilePath : ToString TextFilePath

@[inline]

def Lake.computeFileHash (file : System.FilePath) (text : Bool := false) : IO Hash

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

@[inline]

def Lake.computeArrayHash {α : Type u_1} {m : Type → Type u_2} [ComputeHash α m] [Monad m] (as : Array α) : m Hash

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

@[implicit_reducible]

instance Lake.instComputeHashArrayOfMonad {α : Type u_1} {m : Type → Type u_2} [ComputeHash α m] [Monad m] : ComputeHash (Array α) m

Modification Time (MTime) Trace

def Lake.MTime : Type

A modification time (e.g., of a file).

@[implicit_reducible]

instance Lake.MTime.instOfNat : OfNat MTime 0

@[implicit_reducible]

instance Lake.MTime.instBEq : BEq MTime

@[implicit_reducible]

instance Lake.MTime.instRepr : Repr MTime

@[implicit_reducible]

instance Lake.MTime.instOrd : Ord MTime

@[implicit_reducible]

instance Lake.MTime.instLT : LT MTime

@[implicit_reducible]

instance Lake.MTime.instLE : LE MTime

@[implicit_reducible]

instance Lake.MTime.instMin : Min MTime

@[implicit_reducible]

instance Lake.MTime.instMax : Max MTime

@[implicit_reducible]

instance Lake.MTime.instNilTrace : NilTrace MTime

@[implicit_reducible]

instance Lake.MTime.instMixTrace : MixTrace MTime

class Lake.GetMTime (α : Type u) : Type u

• getMTime : α → IO MTime

  Return the modification time of an object.

@[inline]

def Lake.getFileMTime (file : System.FilePath) : IO MTime

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

@[implicit_reducible]

instance Lake.instGetMTimeFilePath : GetMTime System.FilePath

@[implicit_reducible]

instance Lake.instGetMTimeTextFilePath : GetMTime TextFilePath

@[specialize #[]]

def Lake.MTime.checkUpToDate {i : Type u_1} [GetMTime i] (info : i) (self : MTime) : BaseIO Bool

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

Lake Build Trace

structure Lake.BuildTrace : Type

Trace used for common Lake targets. Combines Hash and MTime.

• caption : String
• inputs : Array BuildTrace
• hash : Hash
• mtime : MTime

partial def Lake.instReprBuildTrace.repr : BuildTrace → Nat → Std.Format

@[implicit_reducible]

instance Lake.instReprBuildTrace : Repr BuildTrace

@[inline]

def Lake.BuildTrace.withCaption (caption : String) (self : BuildTrace) : BuildTrace

Sets the caption of the trace.

@[inline]

def Lake.BuildTrace.withoutInputs (self : BuildTrace) : BuildTrace

Clear the inputs of the build trace. This is used to remove unnecessary repetition of trace trees across multiple trace files.

@[inline]

def Lake.BuildTrace.ofHash (hash : Hash) (caption : String := "<hash>") : BuildTrace

@[implicit_reducible]

instance Lake.BuildTrace.instCoeHash : Coe Hash BuildTrace

@[inline]

def Lake.BuildTrace.ofMTime (mtime : MTime) (caption : String := "<mtime>") : BuildTrace

@[implicit_reducible]

instance Lake.BuildTrace.instCoeMTime : Coe MTime BuildTrace

def Lake.BuildTrace.nil (caption : String := "<nil>") : BuildTrace

@[implicit_reducible]

instance Lake.BuildTrace.instNilTrace : NilTrace BuildTrace

@[specialize #[]]

def Lake.BuildTrace.compute {α : Type u_1} {m : Type → Type u_2} [ToString α] [ComputeHash α m] [MonadLiftT m IO] [GetMTime α] (info : α) : IO BuildTrace

@[implicit_reducible]

instance Lake.BuildTrace.instComputeTraceIOOfToStringOfComputeHashOfMonadLiftTOfGetMTime {α : Type u_1} {m : Type → Type u_2} [ToString α] [ComputeHash α m] [MonadLiftT m IO] [GetMTime α] : ComputeTrace α IO BuildTrace

def Lake.BuildTrace.mix (t1 t2 : BuildTrace) : BuildTrace

@[implicit_reducible]

instance Lake.BuildTrace.instMixTrace : MixTrace BuildTrace

@[specialize #[]]

def Lake.BuildTrace.checkAgainstHash {i : Type u_1} [CheckExists i] (info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool

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.

@[inline]

def Lake.BuildTrace.checkAgainstTime {i : Type u_1} [GetMTime i] (info : i) (self : BuildTrace) : BaseIO Bool

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.