refactor: cleanup trace code some

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)

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

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 :=

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

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)