From ae144112be1ec720066bfc93ca25b63149e46813 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 4 Oct 2021 18:30:24 -0400
Subject: [PATCH] refactor: generalize  `checkModuleTrace`

---
 Lake/BuildModule.lean | 17 ++++++++---------
 Lake/Trace.lean       | 39 +++++++++++++++++++++++++++++++++++++--
 2 files changed, 45 insertions(+), 11 deletions(-)

diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean
index f5e6c6afa1..3f00f8f137 100644
--- a/Lake/BuildModule.lean
+++ b/Lake/BuildModule.lean
@@ -35,6 +35,11 @@ protected def computeHash (self : OleanAndC) : IO Hash := do
 
 instance : ComputeHash OleanAndC := ⟨OleanAndC.computeHash⟩
 
+protected def checkExists (self : OleanAndC) : IO Bool := do
+  return (← checkExists self.oleanFile) && (← checkExists self.cFile)
+
+instance : CheckExists OleanAndC := ⟨OleanAndC.checkExists⟩
+
 end OleanAndC
 
 abbrev ActiveOleanAndCTarget := ActiveBuildTarget OleanAndC
@@ -53,24 +58,18 @@ end ActiveOleanAndCTarget
 
 -- # Trace Checking
 
-def checkModuleTrace [GetMTime i] (info : i)
+def checkModuleTrace [CheckExists i] (info : i)
 (leanFile hashFile : FilePath) (contents : String) (depTrace : BuildTrace)
 : IO (Bool × BuildTrace) := do
   let leanMTime ← getMTime leanFile
   let leanHash := Hash.compute contents
   let maxMTime := max leanMTime depTrace.mtime
   let fullHash := Hash.mix leanHash depTrace.hash
-  try
-    discard <| getMTime info -- check that both output files exist
-    if let some h ← Hash.fromFile hashFile then
-      if h == fullHash then return (true, BuildTrace.fromHash fullHash)
-  catch _ =>
-    pure ()
-  return (false, BuildTrace.mk fullHash maxMTime)
+  BuildTrace.mk fullHash maxMTime |>.check info hashFile
 
 -- # Module Builders
 
-def moduleTarget [GetMTime i] [ComputeHash i] (info : i)
+def moduleTarget [CheckExists i] [GetMTime i] [ComputeHash i] (info : i)
 (leanFile hashFile : FilePath) (contents : String) (depTarget : BuildTarget x)
 (build : BuildM PUnit) : BuildTarget i :=
   Target.mk info <| depTarget.mapOpaqueAsync fun depTrace => do
diff --git a/Lake/Trace.lean b/Lake/Trace.lean
index c7cb8b6cf3..c05bc7de09 100644
--- a/Lake/Trace.lean
+++ b/Lake/Trace.lean
@@ -7,12 +7,25 @@ Authors: Mac Malone
 open System
 namespace Lake
 
+--------------------------------------------------------------------------------
+-- # Utilities
+--------------------------------------------------------------------------------
+
+/-- Check whether there already exists an artifact for the given target info. -/
+class CheckExists.{u} (i : Type u) where
+  checkExists : i → IO Bool
+
+export CheckExists (checkExists)
+
+instance : CheckExists FilePath where
+  checkExists := FilePath.pathExists
+
 --------------------------------------------------------------------------------
 -- # Trace Abstraction
 --------------------------------------------------------------------------------
 
 class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t : Type v) where
-  /-- Compute the trace of some info using information from the monadic context. -/
+  /--  Compute the trace of some target info using information from the monadic context. -/
   computeTrace : i → m t
 
 export ComputeTrace (computeTrace)
@@ -76,7 +89,7 @@ namespace Hash
 def ofNat (n : Nat) :=
   mk n.toUInt64
 
-def fromFile (hashFile : FilePath) : IO (Option Hash) := do
+def loadFromFile (hashFile : FilePath) : IO (Option Hash) := do
   (← IO.FS.readFile hashFile).toNat?.map Hash.ofNat
 
 def nil : Hash :=
@@ -166,9 +179,15 @@ namespace BuildTrace
 def withHash (hash : Hash) (self : BuildTrace) : BuildTrace :=
   {self with hash}
 
+def withouthHash (self : BuildTrace) : BuildTrace :=
+  {self with hash := Hash.nil}
+
 def withMTime (mtime : MTime) (self : BuildTrace) : BuildTrace :=
   {self with mtime}
 
+def withoutMTime (self : BuildTrace) : BuildTrace :=
+  {self with mtime := 0}
+
 def fromHash (hash : Hash) : BuildTrace :=
   mk hash 0
 
@@ -194,4 +213,20 @@ def mix (t1 t2 : BuildTrace) : BuildTrace :=
 
 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]
+(info : i) (hashFile : FilePath) (self : BuildTrace)
+: IO (Bool × BuildTrace) := do
+  try
+    if (← checkExists info) then
+      if let some h ← Hash.loadFromFile hashFile then
+        if h == self.hash then
+          return (true, self.withoutMTime)
+  catch _ =>
+    pure ()
+  return (false, self)
+
 end BuildTrace