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 #
Equations
- Lake.instCheckExistsFilePath = { checkExists := System.FilePath.pathExists }
Trace Abstraction #
Compute the trace of an object in a supporting monad.
Equations
Instances For
- nilTrace : α
The nil trace. Should not unduly clash with a proper trace.
Instances
Equations
- Lake.inhabitedOfNilTrace = { default := Lake.nilTrace }
- mixTrace : α → α → α
Combine two traces. The result should be dirty if either of the inputs is dirty.
Instances
Equations
- Lake.mixTraceList traces = List.foldl Lake.mixTrace Lake.nilTrace traces
Instances For
Equations
- Lake.mixTraceArray traces = Array.foldl Lake.mixTrace Lake.nilTrace traces
Instances For
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
Instances For
Equations
- Lake.instComputeTraceListOfMonad = { computeTrace := Lake.computeListTrace }
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
Instances For
Equations
- Lake.instComputeTraceArrayOfMonad = { computeTrace := Lake.computeArrayTrace }
Hash Trace #
Equations
Equations
- Lake.instReprHash = { reprPrec := Lake.reprHash✝ }
Equations
- Lake.Hash.ofString? s = Option.map Lake.Hash.ofNat (inline s.toNat?)
Instances For
Equations
- Lake.Hash.load? hashFile = EIO.catchExceptions (Lake.Hash.ofString? <$> IO.FS.readFile hashFile) fun (x : IO.Error) => pure none
Instances For
Equations
- Lake.Hash.instNilTrace = { nilTrace := Lake.Hash.nil }
Equations
- Lake.Hash.instMixTrace = { mixTrace := Lake.Hash.mix }
Equations
- Lake.Hash.instToString = { toString := Lake.Hash.toString }
Equations
- Lake.Hash.instToJson = { toJson := Lake.Hash.toJson }
Equations
- Lake.Hash.fromJson? json = (fun (x : UInt64) => { val := x }) <$> Lean.fromJson? json
Instances For
Equations
- Lake.Hash.instFromJson = { fromJson? := Lake.Hash.fromJson? }
Equations
- Lake.instComputeTraceHashOfComputeHash = { computeTrace := Lake.ComputeHash.computeHash }
Compute the hash of object a
in a pure context.
Equations
Instances For
Compute the hash an object in an supporting monad.
Equations
Instances For
Equations
- Lake.instComputeHashStringId = { computeHash := Lake.Hash.ofString }
Compute the hash of a binary file. Binary files are equivalent only if they are byte identical.
Equations
Instances For
Equations
- Lake.instComputeHashFilePathIO = { computeHash := Lake.computeBinFileHash }
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)
Instances For
A wrapper around FilePath
that adjusts its ComputeHash
implementation
to normalize \r\n
sequences to \n
for cross-platform compatibility.
- path : System.FilePath
Instances For
Equations
- Lake.instCoeTextFilePathFilePath = { coe := fun (x : Lake.TextFilePath) => x.path }
Equations
- Lake.instComputeHashTextFilePathIO = { computeHash := fun (x : Lake.TextFilePath) => Lake.computeTextFileHash x.path }
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
Instances For
Compute the hash of each element of an array and combine them (left-to-right).
Equations
Instances For
Equations
- Lake.instComputeHashArrayOfMonad = { computeHash := Lake.computeArrayHash }
Modification Time (MTime) Trace #
A modification time (e.g., of a file).
Equations
Instances For
Equations
- Lake.MTime.instOfNat = { ofNat := { sec := 0, nsec := 0 } }
Equations
Equations
Equations
Equations
- Lake.MTime.instNilTrace = { nilTrace := 0 }
Equations
- Lake.MTime.instMixTrace = { mixTrace := max }
- getMTime : α → IO Lake.MTime
Return the modification time of an object.
Instances
Equations
- Lake.instComputeTraceIOMTimeOfGetMTime = { computeTrace := Lake.getMTime }
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
Instances For
Equations
- Lake.instGetMTimeFilePath = { getMTime := Lake.getFileMTime }
Equations
- Lake.instGetMTimeTextFilePath = { getMTime := fun (x : Lake.TextFilePath) => Lake.getFileMTime x.path }
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.
Instances For
Lake Build Trace #
Trace used for common Lake targets. Combines Hash
and MTime
.
- hash : Lake.Hash
- mtime : Lake.MTime
Instances For
Equations
- Lake.instReprBuildTrace = { reprPrec := Lake.reprBuildTrace✝ }
Equations
- Lake.BuildTrace.instCoeHash = { coe := Lake.BuildTrace.ofHash }
Equations
- Lake.BuildTrace.ofMTime mtime = { hash := Lake.Hash.nil, mtime := mtime }
Instances For
Equations
- Lake.BuildTrace.instCoeMTime = { coe := Lake.BuildTrace.ofMTime }
Equations
- Lake.BuildTrace.nil = { hash := Lake.Hash.nil, mtime := 0 }
Instances For
Equations
- Lake.BuildTrace.instNilTrace = { nilTrace := Lake.BuildTrace.nil }
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 }
Instances For
Equations
- Lake.BuildTrace.instComputeTraceIOOfComputeHashOfMonadLiftTOfGetMTime = { computeTrace := Lake.BuildTrace.compute }
Instances For
Equations
- Lake.BuildTrace.instMixTrace = { mixTrace := Lake.BuildTrace.mix }
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)
Instances For
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
Instances For
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.
Instances For
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