From aa3f453ebf8317d72b67a16c3098047315f7b359 Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 18 Oct 2021 19:38:32 -0400 Subject: [PATCH] refactor: cleanup trace code some --- Lake/BuildModule.lean | 9 +++------ Lake/BuildTarget.lean | 4 ++-- Lake/BuildTargets.lean | 2 +- Lake/Target.lean | 4 ++-- Lake/Trace.lean | 19 +++++++++++-------- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index ecf1529cef..a2a594067a 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -80,13 +80,10 @@ def moduleTarget [CheckExists i] [GetMTime i] [ComputeHash i] (info : i) let srcTrace : BuildTrace := ⟨Hash.ofString contents, ← getMTime leanFile⟩ let fullTrace := leanTrace.mix <| srcTrace.mix depTrace let (upToDate, trace) ← fullTrace.check info traceFile - if upToDate then - BuildTrace.fromHash <| (← computeHash info).mix depTrace.hash - else + unless upToDate do build - IO.FS.writeFile traceFile trace.hash.toString - let newTrace : BuildTrace ← liftM <| computeTrace info - newTrace.mix depTrace + IO.FS.writeFile traceFile trace.hash.toString + pure <| mixTrace (← computeTrace info) depTrace def moduleOleanAndCTarget (leanFile cFile oleanFile traceFile : FilePath) diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean index f33f37cff0..23cb102972 100644 --- a/Lake/BuildTarget.lean +++ b/Lake/BuildTarget.lean @@ -33,11 +33,11 @@ namespace FileTarget variable [ComputeTrace FilePath m BuildTrace] [MonadLiftT m BuildM] def computeSync (path : FilePath) : FileTarget := - Target.mk path do pure <$> try liftM <| computeTrace path catch e => + Target.mk path do pure <$> try computeTrace path catch e => BuildM.logError (toString e); throw e def computeAsync (path : FilePath) : FileTarget := - Target.mk path do async <| try liftM <| computeTrace path catch e => + Target.mk path do async <| try computeTrace path catch e => BuildM.logError (toString e); throw e end FileTarget diff --git a/Lake/BuildTargets.lean b/Lake/BuildTargets.lean index 370ba7feba..f25040904a 100644 --- a/Lake/BuildTargets.lean +++ b/Lake/BuildTargets.lean @@ -21,7 +21,7 @@ def buildFileUnlessUpToDate (file : FilePath) unless upToDate do build IO.FS.writeFile traceFile trace.hash.toString - liftM <| computeTrace file + computeTrace file def fileTargetWithDep (file : FilePath) (depTarget : BuildTarget i) (build : i → BuildM PUnit) : FileTarget := diff --git a/Lake/Target.lean b/Lake/Target.lean index 8274effafb..3bc2ee6a79 100644 --- a/Lake/Target.lean +++ b/Lake/Target.lean @@ -127,10 +127,10 @@ def nil [NilTrace t] [Pure m] [Pure n] : Target PUnit m n t := mk () <| pure <| pure nilTrace def computeSync [ComputeTrace i m' t] [MonadLiftT m' m] [Async m n] [Functor m] [Pure n] (info : i) : Target i m n t := - mk info <| pure <$> liftM (computeTrace info) + mk info <| pure <$> computeTrace info def computeAsync [ComputeTrace i m' t] [MonadLiftT m' m] [Async m n] (info : i) : Target i m n t := - mk info <| async <| liftM <| computeTrace info + mk info <| async <| computeTrace info def run [Monad m] (self : Target i m n t ) : m (ActiveTarget i n t) := Functor.map (fun t => ActiveTarget.mk self.info t) self.task diff --git a/Lake/Trace.lean b/Lake/Trace.lean index f65506d554..8e6bf62b3c 100644 --- a/Lake/Trace.lean +++ b/Lake/Trace.lean @@ -28,7 +28,8 @@ class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t : /-- Compute the trace of some target info using information from the monadic context. -/ computeTrace : i → m t -export ComputeTrace (computeTrace) +def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t := + liftM <| ComputeTrace.computeTrace info class NilTrace.{u} (t : Type u) where /-- The nil trace. Should not unduly clash with a proper trace. -/ @@ -59,17 +60,17 @@ def mixTraceList (traces : List t) : t := def mixTraceArray (traces : Array t) : t := traces.foldl mixTrace nilTrace -variable [ComputeTrace i m t] [Monad m] +variable [ComputeTrace i m t] -def computeListTrace (artifacts : List i) : m t := +def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t := mixTraceList <$> artifacts.mapM computeTrace -instance : ComputeTrace (List i) m t := ⟨computeListTrace⟩ +instance [Monad m] : ComputeTrace (List i) m t := ⟨computeListTrace⟩ -def computeArrayTrace (artifacts : Array i) : m t := +def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t := mixTraceArray <$> artifacts.mapM computeTrace -instance : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩ +instance [Monad m] : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩ end -------------------------------------------------------------------------------- @@ -182,7 +183,7 @@ namespace BuildTrace def withHash (hash : Hash) (self : BuildTrace) : BuildTrace := {self with hash} -def withouthHash (self : BuildTrace) : BuildTrace := +def withoutHash (self : BuildTrace) : BuildTrace := {self with hash := Hash.nil} def withMTime (mtime : MTime) (self : BuildTrace) : BuildTrace := @@ -220,7 +221,7 @@ instance : MixTrace BuildTrace := ⟨mix⟩ Check the build trace against the given target info and hash to see if the target is up-to-date. -/ -def check [CheckExists i] +def check [CheckExists i] [GetMTime i] (info : i) (traceFile : FilePath) (self : BuildTrace) : IO (Bool × BuildTrace) := do try @@ -228,6 +229,8 @@ def check [CheckExists i] if let some h ← Hash.loadFromFile traceFile then if h == self.hash then return (true, self.withoutMTime) + else if self.mtime < (← getMTime info) then + return (true, self) catch _ => pure () return (false, self)