Lake.Build.Trace

source

class Lake.CheckExists (i : Type u) :

Type u

checkExists : i → BaseIO Bool
Check whether there already exists an artifact for the given target info.

Instances

source

instance Lake.instCheckExistsFilePath :

Lake.CheckExists Lake.FilePath

Equations

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

source

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.

Instances

source

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

source

class Lake.NilTrace (t : Type u) :

Type u

nilTrace : t
The nil trace. Should not unduly clash with a proper trace.

Instances

source

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

Inhabited t

Equations

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

source

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.

Instances

source

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

source

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

source

@[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) (t_1 : i) => do let __do_lift ← Lake.computeTrace t_1 pure (Lake.mixTrace ts __do_lift)) Lake.nilTrace artifacts

source

instance Lake.instComputeTraceListOfMonad {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.instComputeTraceListOfMonad = { computeTrace := Lake.computeListTrace }

source

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

Lake.computeArrayTrace artifacts = Array.foldlM (fun (ts : t) (t_1 : i) => do let __do_lift ← Lake.computeTrace t_1 pure (Lake.mixTrace ts __do_lift)) Lake.nilTrace artifacts

source

instance Lake.instComputeTraceArrayOfMonad {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.instComputeTraceArrayOfMonad = { computeTrace := Lake.computeArrayTrace }

source

structure Lake.Hash :

Type

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

val : UInt64

Instances For

source

instance Lake.instBEqHash :

BEq Lake.Hash

Equations

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

source

instance Lake.instDecidableEqHash :

DecidableEq Lake.Hash

Equations

Lake.instDecidableEqHash = Lake.decEqHash✝

source

instance Lake.instReprHash :

Repr Lake.Hash

Equations

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

source

@[inline]

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

Lake.Hash

Equations

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

source

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

Option Lake.Hash

Equations

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

source

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

BaseIO (Option Lake.Hash)

Equations

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

source

def Lake.Hash.nil :

Lake.Hash

Equations

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

source

instance Lake.Hash.instNilTrace :

Lake.NilTrace Lake.Hash

Equations

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

source

@[inline]

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

Lake.Hash

Equations

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

source

instance Lake.Hash.instMixTrace :

Lake.MixTrace Lake.Hash

Equations

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

source

@[inline]

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

String

Equations

self.toString = toString self.val

source

instance Lake.Hash.instToString :

ToString Lake.Hash

Equations

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

source

@[inline]

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

Lake.Hash

Equations

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

source

@[inline]

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

Lake.Hash

Equations

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

source

@[inline]

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

Lean.Json

Equations

self.toJson = Lean.toJson self.val

source

instance Lake.Hash.instToJson :

Lean.ToJson Lake.Hash

Equations

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

source

@[inline]

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

Except String Lake.Hash

Equations

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

source

instance Lake.Hash.instFromJson :

Lean.FromJson Lake.Hash

Equations

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

source

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

Type (max u v)

computeHash : α → m Lake.Hash

Instances

source

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

Lake.ComputeTrace α m Lake.Hash

Equations

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

source

@[inline]

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

Lake.Hash

Equations

Lake.pureHash a = Lake.ComputeHash.computeHash a

source

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

source

instance Lake.instComputeHashStringId :

Lake.ComputeHash String Id

Equations

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

source

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

IO Lake.Hash

Equations

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

source

instance Lake.instComputeHashFilePathIO :

Lake.ComputeHash Lake.FilePath IO

Equations

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

source

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

IO Lake.Hash

Equations

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

source

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

Instances For

source

instance Lake.instCoeTextFilePathFilePath :

Coe Lake.TextFilePath Lake.FilePath

Equations

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

source

instance Lake.instComputeHashTextFilePathIO :

Lake.ComputeHash Lake.TextFilePath IO

Equations

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

source

@[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 : Lake.Hash) (a : α) => do let __do_lift ← Lake.computeHash a pure (h.mix __do_lift)) Lake.Hash.nil xs

source

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

Lake.ComputeHash (Array α) m

Equations

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

source

def Lake.MTime :

Type

A modification time.

Equations

Lake.MTime = IO.FS.SystemTime

Instances For

source

instance Lake.MTime.instOfNat :

OfNat Lake.MTime 0

Equations

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

source

instance Lake.MTime.instBEq :

BEq Lake.MTime

Equations

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

source

instance Lake.MTime.instRepr :

Repr Lake.MTime

Equations

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

source

instance Lake.MTime.instOrd :

Ord Lake.MTime

Equations

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

source

instance Lake.MTime.instLT :

LT Lake.MTime

Equations

Lake.MTime.instLT = ltOfOrd

source

instance Lake.MTime.instLE :

LE Lake.MTime

Equations

Lake.MTime.instLE = leOfOrd

source

instance Lake.MTime.instMin :

Min Lake.MTime

Equations

Lake.MTime.instMin = minOfLe

source

instance Lake.MTime.instMax :

Max Lake.MTime

Equations

Lake.MTime.instMax = maxOfLe

source

instance Lake.MTime.instNilTrace :

Lake.NilTrace Lake.MTime

Equations

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

source

instance Lake.MTime.instMixTrace :

Lake.MixTrace Lake.MTime

Equations

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

source

class Lake.GetMTime (α : Sort u_1) :

Sort (max 1 u_1)

getMTime : α → IO Lake.MTime

Instances

source

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

Lake.ComputeTrace α IO Lake.MTime

Equations

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

source

@[inline]

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

IO Lake.MTime

Equations

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

source

instance Lake.instGetMTimeFilePath :

Lake.GetMTime Lake.FilePath

Equations

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

source

instance Lake.instGetMTimeTextFilePath :

Lake.GetMTime Lake.TextFilePath

Equations

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

source

@[specialize #[]]

def Lake.MTime.checkUpToDate {i : Sort u_1} [Lake.GetMTime i] (info : i) (self : Lake.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.

source

structure Lake.BuildTrace :

Type

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

hash : Lake.Hash
mtime : Lake.MTime

Instances For

source

instance Lake.instReprBuildTrace :

Repr Lake.BuildTrace

Equations

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

source

@[inline]

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

Lake.BuildTrace

Equations

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

source

instance Lake.BuildTrace.instCoeHash :

Coe Lake.Hash Lake.BuildTrace

Equations

Lake.BuildTrace.instCoeHash = { coe := Lake.BuildTrace.ofHash }

source

@[inline]

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

Lake.BuildTrace

Equations

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

source

instance Lake.BuildTrace.instCoeMTime :

Coe Lake.MTime Lake.BuildTrace

Equations

Lake.BuildTrace.instCoeMTime = { coe := Lake.BuildTrace.ofMTime }

source

def Lake.BuildTrace.nil :

Lake.BuildTrace

Equations

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

source

instance Lake.BuildTrace.instNilTrace :

Lake.NilTrace Lake.BuildTrace

Equations

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

source

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

source

instance Lake.BuildTrace.instComputeTraceIOOfComputeHashOfMonadLiftTOfGetMTime {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.instComputeTraceIOOfComputeHashOfMonadLiftTOfGetMTime = { computeTrace := Lake.BuildTrace.compute }

source

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

Lake.BuildTrace

Equations

t1.mix t2 = { hash := t1.hash.mix t2.hash, mtime := max t1.mtime t2.mtime }

source

instance Lake.BuildTrace.instMixTrace :

Lake.MixTrace Lake.BuildTrace

Equations

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

source

@[specialize #[]]

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)

source

@[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 = Lake.MTime.checkUpToDate info self.mtime

source

@[specialize #[], deprecated]

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.

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

Equations

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

source

@[deprecated]

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

IO PUnit

Write trace to a file.

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

Equations

Lake.BuildTrace.writeToFile traceFile self = do Lake.createParentDirs traceFile IO.FS.writeFile traceFile self.hash.toString

Documentation

Lake.Build.Trace

Utilities #

Trace Abstraction #

Hash Trace #

Modification Time (MTime) Trace #

Lake Build Trace (Hash + MTIme) #