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 : Lake.CheckExists Lake.FilePath

Equations

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

Trace Abstraction

class Lake.ComputeTrace (i : Type u) (m : outParam (Type v → Type w)) (t : Type v) : Type (max u w)

• computeTrace : i → m t

  Compute the trace of some target info using information from the monadic context.

@[inline]

def Lake.computeTrace {i : Type u_1} {m : Type u_2 → Type u_3} {t : Type u_2} {n : Type u_2 → Type u_4} [Lake.ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t

Equations

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

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

• nilTrace : t

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

instance Lake.instInhabited {t : Type u_1} [Lake.NilTrace t] : Inhabited t

Equations

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

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

• mixTrace : t → t → t

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

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

Equations

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

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

Equations

• Lake.mixTraceArray traces = Array.foldl Lake.mixTrace Lake.nilTrace traces 0 (Array.size traces)

@[specialize #[]]

def Lake.computeListTrace {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (artifacts : List i) : n t

Equations

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

instance Lake.instComputeTraceList {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] [Monad m] : Lake.ComputeTrace (List i) m t

Equations

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

@[specialize #[]]

def Lake.computeArrayTrace {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t

Equations

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

instance Lake.instComputeTraceArray {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] [Monad m] : Lake.ComputeTrace (Array i) m t

Equations

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

Hash Trace

structure Lake.Hash : Type

• val : UInt64

A content hash. TODO: Use a secure hash rather than the builtin Lean hash function.

instance Lake.instBEqHash : BEq Lake.Hash

Equations

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

instance Lake.instDecidableEqHash : DecidableEq Lake.Hash

Equations

• Lake.instDecidableEqHash = Lake.decEqHash✝

instance Lake.instReprHash : Repr Lake.Hash

Equations

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

@[inline]

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

Equations

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

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

Equations

• Lake.Hash.load? hashFile = EIO.catchExceptions ((fun x => Option.map Lake.Hash.ofNat (String.toNat? x)) <$> IO.FS.readFile hashFile) fun x => pure none

def Lake.Hash.nil : Lake.Hash

Equations

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

instance Lake.Hash.instNilTraceHash : Lake.NilTrace Lake.Hash

Equations

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

@[inline]

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

Equations

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

instance Lake.Hash.instMixTraceHash : Lake.MixTrace Lake.Hash

Equations

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

@[inline]

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

Equations

• Lake.Hash.toString self = toString self.val

instance Lake.Hash.instToStringHash : ToString Lake.Hash

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

• computeHash : α → m Lake.Hash

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

Equations

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

@[inline]

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

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} [Lake.ComputeHash α m] [MonadLiftT m n] (a : α) : n Lake.Hash

Equations

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

instance Lake.instComputeHashStringId : Lake.ComputeHash String Id

Equations

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

def Lake.computeFileHash (file : Lake.FilePath) : IO Lake.Hash

Equations

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

instance Lake.instComputeHashFilePathIO : Lake.ComputeHash Lake.FilePath IO

Equations

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

@[inline]

def Lake.crlf2lf (text : String) : String

This is the same as String.replace text "\r\n" "\n", but more efficient.

Equations

• Lake.crlf2lf text = Lake.crlf2lf.go text "" 0 0

partial def Lake.crlf2lf.go (text : String) (acc : String) (accStop : String.Pos) (pos : String.Pos) : String

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

Equations

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

structure Lake.TextFilePath : Type

• path : Lake.FilePath

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

instance Lake.instCoeTextFilePathFilePath : Coe Lake.TextFilePath Lake.FilePath

Equations

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

instance Lake.instComputeHashTextFilePathIO : Lake.ComputeHash Lake.TextFilePath IO

Equations

• Lake.instComputeHashTextFilePathIO = { computeHash := fun file => Lake.computeTextFileHash file.path }

@[specialize #[]]

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

Equations

• Lake.computeArrayHash xs = Array.foldlM (fun h a => do let __do_lift ← Lake.computeHash a pure (Lake.Hash.mix h __do_lift)) Lake.Hash.nil xs 0 (Array.size xs)

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

Equations

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

Modification Time (MTime) Trace

def Lake.MTime : Type

A modification time.

Equations

• Lake.MTime = IO.FS.SystemTime

instance Lake.MTime.instOfNatMTime : OfNat Lake.MTime 0

Equations

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

instance Lake.MTime.instBEqMTime : BEq Lake.MTime

Equations

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

instance Lake.MTime.instReprMTime : Repr Lake.MTime

Equations

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

instance Lake.MTime.instOrdMTime : Ord Lake.MTime

Equations

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

instance Lake.MTime.instLTMTime : LT Lake.MTime

Equations

• Lake.MTime.instLTMTime = ltOfOrd

instance Lake.MTime.instLEMTime : LE Lake.MTime

Equations

• Lake.MTime.instLEMTime = leOfOrd

instance Lake.MTime.instMinMTime : Min Lake.MTime

Equations

• Lake.MTime.instMinMTime = minOfLe

instance Lake.MTime.instMaxMTime : Max Lake.MTime

Equations

• Lake.MTime.instMaxMTime = maxOfLe

instance Lake.MTime.instNilTraceMTime : Lake.NilTrace Lake.MTime

Equations

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

instance Lake.MTime.instMixTraceMTime : Lake.MixTrace Lake.MTime

Equations

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

class Lake.GetMTime (α : Sort u_1) : Sort (max 1 u_1)

• getMTime : α → IO Lake.MTime

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

Equations

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

@[inline]

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

Equations

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

instance Lake.instGetMTimeFilePath : Lake.GetMTime Lake.FilePath

Equations

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

instance Lake.instGetMTimeTextFilePath : Lake.GetMTime Lake.TextFilePath

Equations

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

Lake Build Trace (Hash + MTIme)

structure Lake.BuildTrace : Type

• hash : Lake.Hash
• mtime : Lake.MTime

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

instance Lake.instReprBuildTrace : Repr Lake.BuildTrace

Equations

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

@[inline]

def Lake.BuildTrace.ofHash (hash : Lake.Hash) : Lake.BuildTrace

Equations

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

instance Lake.BuildTrace.instCoeHashBuildTrace : Coe Lake.Hash Lake.BuildTrace

Equations

• Lake.BuildTrace.instCoeHashBuildTrace = { coe := Lake.BuildTrace.ofHash }

@[inline]

def Lake.BuildTrace.ofMTime (mtime : Lake.MTime) : Lake.BuildTrace

Equations

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

instance Lake.BuildTrace.instCoeMTimeBuildTrace : Coe Lake.MTime Lake.BuildTrace

Equations

• Lake.BuildTrace.instCoeMTimeBuildTrace = { coe := Lake.BuildTrace.ofMTime }

def Lake.BuildTrace.nil : Lake.BuildTrace

Equations

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

instance Lake.BuildTrace.instNilTraceBuildTrace : Lake.NilTrace Lake.BuildTrace

Equations

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

@[specialize #[]]

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

Equations

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

instance Lake.BuildTrace.instComputeTraceIOBuildTrace {i : Type u_1} {m : Type → Type u_2} [Lake.ComputeHash i m] [MonadLiftT m IO] [Lake.GetMTime i] : Lake.ComputeTrace i IO Lake.BuildTrace

Equations

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

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

Equations

• Lake.BuildTrace.mix t1 t2 = { hash := Lake.Hash.mix t1.hash t2.hash, mtime := max t1.mtime t2.mtime }

instance Lake.BuildTrace.instMixTraceBuildTrace : Lake.MixTrace Lake.BuildTrace

Equations

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

@[inline]

def Lake.BuildTrace.checkAgainstHash {i : Type u_1} [Lake.CheckExists i] (info : i) (hash : Lake.Hash) (self : Lake.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 : Sort u_1} [Lake.GetMTime i] (info : i) (self : Lake.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 = EIO.catchExceptions (do let __do_lift ← Lake.getMTime info pure (decide (self.mtime < __do_lift))) fun x => pure false

@[inline]

def Lake.BuildTrace.checkAgainstFile {i : Type u_1} [Lake.CheckExists i] [Lake.GetMTime i] (info : i) (traceFile : Lake.FilePath) (self : Lake.BuildTrace) : BaseIO Bool

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.

Equations

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

@[inline]

def Lake.BuildTrace.writeToFile (traceFile : Lake.FilePath) (self : Lake.BuildTrace) : IO PUnit

Equations

• Lake.BuildTrace.writeToFile traceFile self = IO.FS.writeFile traceFile (Lake.Hash.toString self.hash)