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.

instance Lake.instCheckExistsFilePath : CheckExists System.FilePath

Equations

• Lake.instCheckExistsFilePath = { checkExists := System.FilePath.pathExists }

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.

Equations

• Lake.computeTrace a = liftM (Lake.ComputeTrace.computeTrace a)

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

• nilTrace : α

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

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

Equations

• Lake.inhabitedOfNilTrace = { default := Lake.nilTrace }

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 τ) : τ

Equations

• Lake.mixTraceList traces = List.foldl Lake.mixTrace Lake.nilTrace traces

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

Equations

• Lake.mixTraceArray traces = Array.foldl Lake.mixTrace Lake.nilTrace traces

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

• Lake.computeListTrace as = List.foldlM (fun (ts : τ) (t : α) => do let __do_lift ← Lake.computeTrace t pure (Lake.mixTrace ts __do_lift)) Lake.nilTrace as

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

• Lake.instComputeTraceListOfMonad = { computeTrace := Lake.computeListTrace }

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

• Lake.computeArrayTrace as = Array.foldlM (fun (ts : τ) (t : α) => do let __do_lift ← Lake.computeTrace t pure (Lake.mixTrace ts __do_lift)) Lake.nilTrace as

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 τ

Equations

• Lake.instComputeTraceArrayOfMonad = { computeTrace := Lake.computeArrayTrace }

Hash Trace

structure Lake.Hash : Type

A content hash.

• val : UInt64

instance Lake.instBEqHash : BEq Hash

Equations

• Lake.instBEqHash = { beq := Lake.beqHash✝ }

instance Lake.instDecidableEqHash : DecidableEq Hash

Equations

• Lake.instDecidableEqHash = Lake.decEqHash✝

instance Lake.instReprHash : Repr Hash

Equations

• Lake.instReprHash = { reprPrec := Lake.reprHash✝ }

@[inline]

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

Equations

• Lake.Hash.ofNat n = { val := n.toUInt64 }

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

Equations

• Lake.Hash.ofString? s = Option.map Lake.Hash.ofNat (inline s.toNat?)

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

Equations

• Lake.Hash.load? hashFile = EIO.catchExceptions (Lake.Hash.ofString? <$> IO.FS.readFile hashFile) fun (x : IO.Error) => pure none

def Lake.Hash.nil : Hash

Equations

• Lake.Hash.nil = { val := 1723 }

instance Lake.Hash.instNilTrace : NilTrace Hash

Equations

• Lake.Hash.instNilTrace = { nilTrace := Lake.Hash.nil }

@[inline]

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

Equations

• h1.mix h2 = { val := mixHash h1.val h2.val }

instance Lake.Hash.instMixTrace : MixTrace Hash

Equations

• Lake.Hash.instMixTrace = { mixTrace := Lake.Hash.mix }

@[inline]

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

Equations

• self.toString = toString self.val

instance Lake.Hash.instToString : ToString Hash

Equations

• Lake.Hash.instToString = { toString := Lake.Hash.toString }

@[inline]

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

Equations

• Lake.Hash.ofString str = Lake.Hash.nil.mix { val := hash str }

@[inline]

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

Equations

• Lake.Hash.ofByteArray bytes = { val := hash bytes }

@[inline]

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

Equations

• Lake.Hash.ofBool b = { val := hash b }

@[inline]

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

Equations

• self.toJson = Lean.toJson self.val

instance Lake.Hash.instToJson : Lean.ToJson Hash

Equations

• Lake.Hash.instToJson = { toJson := Lake.Hash.toJson }

@[inline]

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

Equations

• Lake.Hash.fromJson? json = (fun (x : UInt64) => { val := x }) <$> Lean.fromJson? json

instance Lake.Hash.instFromJson : Lean.FromJson Hash

Equations

• Lake.Hash.instFromJson = { fromJson? := Lake.Hash.fromJson? }

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.

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

Equations

• Lake.instComputeTraceHashOfComputeHash = { computeTrace := Lake.ComputeHash.computeHash }

@[inline]

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

Compute the hash of object a in a pure context.

Equations

• Lake.pureHash a = Lake.ComputeHash.computeHash a

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

Equations

• Lake.computeHash a = liftM (Lake.ComputeHash.computeHash a)

instance Lake.instComputeHashBoolId : ComputeHash Bool Id

Equations

• Lake.instComputeHashBoolId = { computeHash := Lake.Hash.ofBool }

instance Lake.instComputeHashStringId : ComputeHash String Id

Equations

• Lake.instComputeHashStringId = { computeHash := Lake.Hash.ofString }

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.

Equations

• Lake.computeBinFileHash file = Lake.Hash.ofByteArray <$> IO.FS.readBinFile file

instance Lake.instComputeHashFilePathIO : ComputeHash System.FilePath IO

Equations

• Lake.instComputeHashFilePathIO = { computeHash := Lake.computeBinFileHash }

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.

Equations

• Lake.computeTextFileHash file = do let text ← IO.FS.readFile file let text : String := text.crlfToLf pure (Lake.Hash.ofString text)

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

instance Lake.instCoeTextFilePathFilePath : Coe TextFilePath System.FilePath

Equations

• Lake.instCoeTextFilePathFilePath = { coe := fun (x : Lake.TextFilePath) => x.path }

instance Lake.instComputeHashTextFilePathIO : ComputeHash TextFilePath IO

Equations

• Lake.instComputeHashTextFilePathIO = { computeHash := fun (x : Lake.TextFilePath) => Lake.computeTextFileHash x.path }

instance Lake.instToStringTextFilePath : ToString TextFilePath

Equations

• Lake.instToStringTextFilePath = { toString := fun (x : Lake.TextFilePath) => x.path.toString }

@[inline]

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

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

Equations

• Lake.computeFileHash file text = if text = true then Lake.computeTextFileHash file else Lake.computeBinFileHash file

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

Equations

• Lake.computeArrayHash as = Lake.computeArrayTrace as

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

Equations

• Lake.instComputeHashArrayOfMonad = { computeHash := Lake.computeArrayHash }

Modification Time (MTime) Trace

def Lake.MTime : Type

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

Equations

• Lake.MTime = IO.FS.SystemTime

instance Lake.MTime.instOfNat : OfNat MTime 0

Equations

• Lake.MTime.instOfNat = { ofNat := { sec := 0, nsec := 0 } }

instance Lake.MTime.instBEq : BEq MTime

Equations

• Lake.MTime.instBEq = inferInstanceAs (BEq IO.FS.SystemTime)

instance Lake.MTime.instRepr : Repr MTime

Equations

• Lake.MTime.instRepr = inferInstanceAs (Repr IO.FS.SystemTime)

instance Lake.MTime.instOrd : Ord MTime

Equations

• Lake.MTime.instOrd = inferInstanceAs (Ord IO.FS.SystemTime)

instance Lake.MTime.instLT : LT MTime

Equations

• Lake.MTime.instLT = ltOfOrd

instance Lake.MTime.instLE : LE MTime

Equations

• Lake.MTime.instLE = leOfOrd

instance Lake.MTime.instMin : Min MTime

Equations

• Lake.MTime.instMin = minOfLe

instance Lake.MTime.instMax : Max MTime

Equations

• Lake.MTime.instMax = maxOfLe

instance Lake.MTime.instNilTrace : NilTrace MTime

Equations

• Lake.MTime.instNilTrace = { nilTrace := 0 }

instance Lake.MTime.instMixTrace : MixTrace MTime

Equations

• Lake.MTime.instMixTrace = { mixTrace := max }

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

• getMTime : α → IO MTime

  Return the modification time of an object.

instance Lake.instComputeTraceIOMTimeOfGetMTime {α : Type u_1} [GetMTime α] : ComputeTrace α IO MTime

Equations

• Lake.instComputeTraceIOMTimeOfGetMTime = { computeTrace := Lake.getMTime }

@[inline]

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

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

Equations

• Lake.getFileMTime file = do let __do_lift ← file.metadata pure __do_lift.modified

instance Lake.instGetMTimeFilePath : GetMTime System.FilePath

Equations

• Lake.instGetMTimeFilePath = { getMTime := Lake.getFileMTime }

instance Lake.instGetMTimeTextFilePath : GetMTime TextFilePath

Equations

• Lake.instGetMTimeTextFilePath = { getMTime := fun (x : Lake.TextFilePath) => Lake.getFileMTime x.path }

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

Equations

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

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

instance Lake.instReprBuildTrace : Repr BuildTrace

Equations

• Lake.instReprBuildTrace = { reprPrec := Lake.reprBuildTrace✝ }

@[inline]

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

Sets the caption of the trace.

Equations

• Lake.BuildTrace.withCaption caption self = { caption := caption, inputs := self.inputs, hash := self.hash, mtime := self.mtime }

@[inline]

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

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

Equations

• self.withoutInputs = { caption := self.caption, hash := self.hash, mtime := self.mtime }

@[inline]

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

Equations

• Lake.BuildTrace.ofHash hash caption = { caption := caption, hash := hash, mtime := 0 }

instance Lake.BuildTrace.instCoeHash : Coe Hash BuildTrace

Equations

• Lake.BuildTrace.instCoeHash = { coe := fun (hash : Lake.Hash) => Lake.BuildTrace.ofHash hash }

@[inline]

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

Equations

• Lake.BuildTrace.ofMTime mtime caption = { caption := caption, hash := Lake.Hash.nil, mtime := mtime }

instance Lake.BuildTrace.instCoeMTime : Coe MTime BuildTrace

Equations

• Lake.BuildTrace.instCoeMTime = { coe := fun (mtime : Lake.MTime) => Lake.BuildTrace.ofMTime mtime }

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

Equations

• Lake.BuildTrace.nil caption = { caption := caption, hash := Lake.Hash.nil, mtime := 0 }

instance Lake.BuildTrace.instNilTrace : NilTrace BuildTrace

Equations

• Lake.BuildTrace.instNilTrace = { nilTrace := Lake.BuildTrace.nil }

@[specialize #[]]

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

Equations

• Lake.BuildTrace.compute info = do let __do_lift ← Lake.computeHash info let __do_lift_1 ← Lake.getMTime info pure { caption := toString info, hash := __do_lift, mtime := __do_lift_1 }

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

Equations

• Lake.BuildTrace.instComputeTraceIOOfToStringOfComputeHashOfMonadLiftTOfGetMTime = { computeTrace := Lake.BuildTrace.compute }

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

Equations

• t1.mix t2 = { caption := t1.caption, inputs := t1.inputs.push t2, hash := t1.hash.mix t2.hash, mtime := max t1.mtime t2.mtime }

instance Lake.BuildTrace.instMixTrace : MixTrace BuildTrace

Equations

• Lake.BuildTrace.instMixTrace = { mixTrace := Lake.BuildTrace.mix }

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

Equations

• Lake.BuildTrace.checkAgainstHash info hash self = (pure (hash == self.hash) <&&> Lake.checkExists info)

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

Equations

• Lake.BuildTrace.checkAgainstTime info self = Lake.MTime.checkUpToDate info self.mtime