From 115fdbea98d22e996c9a05413d421d1ad984199e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 13 Jul 2021 15:29:59 -0400
Subject: [PATCH] refactor: simplify mtime checking code

---
 Lake/Build.lean       | 36 +++++++++++++++++++-----------------
 Lake/BuildTarget.lean |  1 +
 2 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/Lake/Build.lean b/Lake/Build.lean
index df0793cb51..ce8cb65f74 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -69,6 +69,25 @@ def moduleTargets (self : PackageTarget) : NameMap LeanTarget :=
 
 end PackageTarget
 
+-- # MTime Checking
+
+/-- Check if the artifact's `MTIme` is at least `depMTime`. -/
+def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do
+  try (← getMTime artifact) >= depMTime catch _ => false
+
+/--
+  Construct a no-op target if the given artifact is up-to-date.
+  Otherwise, construct a target with the given build task.
+-/
+def skipIfNewer [GetMTime a]
+(artifact : a) (depMTime : MTime)
+{m} [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m]
+(build : m BuildTask) : m (MTimeBuildTarget a) := do
+  if (← checkIfNewer artifact depMTime) then
+    MTimeBuildTarget.pure artifact depMTime
+  else
+    MTimeBuildTarget.mk artifact depMTime (← build)
+
 -- # Build Components
 
 def catchErrors (action : IO PUnit) : IO PUnit := do
@@ -77,20 +96,6 @@ def catchErrors (action : IO PUnit) : IO PUnit := do
     IO.eprintln e
     throw e
 
-def skipIfNewer [GetMTime a]
-(artifact : a) (depMTime : MTime)
-{m} [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m]
-(build : m BuildTask) : m (MTimeBuildTarget a) := do
-  -- construct a nop target if we have an up-to-date file
-  try
-    if (← getMTime artifact) >= depMTime then
-      return MTimeBuildTarget.pure artifact depMTime
-  catch
-    | IO.Error.noFileOrDirectory .. => pure ()
-    | e => throw e
-  -- otherwise construct a proper target
-  return MTimeBuildTarget.mk artifact depMTime (← build)
-
 def buildO (oFile : FilePath)
 (cTarget : FileTarget) (leancArgs : Array String := #[]) : IO BuildTask :=
   BuildTask.afterTarget cTarget <| catchErrors <|
@@ -98,7 +103,6 @@ def buildO (oFile : FilePath)
 
 def fetchOFileTarget (oFile : FilePath)
 (cTarget : FileTarget) (leancArgs : Array String := #[]) : IO FileTarget :=
-  -- construct a nop target if we have an up-to-date .o
   skipIfNewer oFile cTarget.mtime <| buildO oFile cTarget leancArgs
 
 -- # Topological Builder
@@ -307,7 +311,6 @@ def PackageTarget.buildStaticLib
 
 def PackageTarget.fetchStaticLibTarget
 (self : PackageTarget) : IO FileTarget := do
-  -- construct a nop target if we have an up-to-date lib
   skipIfNewer self.package.staticLibFile self.mtime self.buildStaticLib
 
 def Package.fetchStaticLibTarget (self : Package) : IO FileTarget := do
@@ -338,7 +341,6 @@ def PackageTarget.buildBin
 
 def PackageTarget.fetchBinTarget
 (depTargets : List PackageTarget) (self : PackageTarget) : IO FileTarget :=
-  -- construct a nop target if we have an up-to-date bin
   skipIfNewer self.package.binFile self.mtime <| self.buildBin depTargets
 
 def Package.fetchBinTarget (self : Package) : IO FileTarget := do
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 1db9e8c900..fb58264fe8 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -29,6 +29,7 @@ end BuildTask
 
 instance : Inhabited BuildTask := ⟨BuildTask.nop⟩
 
+
 structure BuildTarget (t : Type) (a : Type) where
   artifact    : a
   trace       : t