From 752bc24f7862a6b50aa06ca5cf2b68d642d924c9 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 27 Dec 2021 12:07:15 -0500
Subject: [PATCH] feat: add args to binary & `.o` file traces + some cleanup

closes leanprover/lake#41
---
 Lake/Build/Targets.lean | 45 ++++++++++++++++++++---------------------
 1 file changed, 22 insertions(+), 23 deletions(-)

diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean
index 143bdb4805..f86d2c7511 100644
--- a/Lake/Build/Targets.lean
+++ b/Lake/Build/Targets.lean
@@ -16,43 +16,42 @@ def inputFileTarget (path : FilePath) : FileTarget :=
 
 instance : Coe FilePath FileTarget := ⟨inputFileTarget⟩
 
+def buildUnlessUpToDate [CheckExists i] [GetMTime i] (info : i)
+(depTrace : BuildTrace) (traceFile : FilePath) (build : BuildM PUnit) : BuildM PUnit := do
+  let upToDate ← depTrace.checkAgainstFile info traceFile
+  unless upToDate do
+    build
+    depTrace.writeToFile traceFile
+
 def buildFileUnlessUpToDate (file : FilePath)
 (depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"
-  let upToDate ← depTrace.checkAgainstFile file traceFile
-  unless upToDate do
-    build
-  depTrace.writeToFile traceFile
+  buildUnlessUpToDate file depTrace traceFile build
   computeTrace file
 
-def fileTargetWithDep (file : FilePath)
-(depTarget : BuildTarget i) (build : i → BuildM PUnit) : FileTarget :=
-  Target.mk file do
-    depTarget.bindSync fun depInfo depTrace =>
-      buildFileUnlessUpToDate file depTrace <| build depInfo
+def fileTargetWithDep (file : FilePath) (depTarget : BuildTarget i)
+(build : i → BuildM PUnit) (extraDepTrace := BuildTrace.nil) : FileTarget :=
+  Target.mk file <| depTarget.bindSync fun depInfo depTrace =>
+    buildFileUnlessUpToDate file (depTrace.mix extraDepTrace) <| build depInfo
 
-def fileTargetWithDepList (file : FilePath)
-(depTargets : List (BuildTarget i)) (build : List i → BuildM PUnit) : FileTarget :=
-  Target.mk file do
-    Target.collectList depTargets |>.bindSync fun depInfos depTrace =>
-      buildFileUnlessUpToDate file depTrace <| build depInfos
+def fileTargetWithDepList (file : FilePath) (depTargets : List (BuildTarget i))
+(build : List i → BuildM PUnit) (extraDepTrace := BuildTrace.nil) : FileTarget :=
+  fileTargetWithDep file (Target.collectList depTargets) build extraDepTrace
 
-def fileTargetWithDepArray (file : FilePath)
-(depTargets : Array (BuildTarget i)) (build : Array i → BuildM PUnit) : FileTarget :=
-  Target.mk file do
-    Target.collectArray depTargets |>.bindSync fun depInfos depTrace =>
-      buildFileUnlessUpToDate file depTrace <| build depInfos
+def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget i))
+(build : Array i → BuildM PUnit) (extraDepTrace := BuildTrace.nil) : FileTarget :=
+  fileTargetWithDep file (Target.collectArray depTargets) build extraDepTrace
 
 -- # Specific Targets
 
 def oFileTarget (oFile : FilePath) (srcTarget : FileTarget)
 (args : Array String := #[]) (compiler : FilePath := "c++") : FileTarget :=
-  fileTargetWithDep oFile srcTarget fun srcFile => do
+  fileTargetWithDep oFile srcTarget (extraDepTrace := pureHash args) fun srcFile => do
     compileO oFile srcFile args compiler
 
 def leanOFileTarget (oFile : FilePath)
 (srcTarget : FileTarget) (args : Array String := #[]) : FileTarget :=
-  fileTargetWithDep oFile srcTarget fun srcFile => do
+  fileTargetWithDep oFile srcTarget (extraDepTrace := pureHash args) fun srcFile => do
     compileO oFile srcFile args (← getLeanc)
 
 def staticLibTarget (libFile : FilePath)
@@ -67,10 +66,10 @@ def leanSharedLibTarget (binFile : FilePath)
 
 def binTarget (binFile : FilePath) (linkTargets : Array FileTarget)
 (linkArgs : Array String := #[]) (linker : FilePath := "cc") : FileTarget :=
-   fileTargetWithDepArray binFile linkTargets fun links => do
+   fileTargetWithDepArray binFile linkTargets (extraDepTrace := pureHash linkArgs) fun links => do
     compileBin binFile links linkArgs linker
 
 def leanBinTarget (binFile : FilePath)
 (linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
-  fileTargetWithDepArray binFile linkTargets fun links => do
+  fileTargetWithDepArray binFile linkTargets (extraDepTrace := pureHash linkArgs) fun links => do
     compileBin binFile links linkArgs (← getLeanc)