From aa1ca9c4b72de3e15ddfea8972619e21facd0443 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 4 Aug 2021 14:07:28 -0400
Subject: [PATCH] feat: improve Target API

---
 Lake.lean                 |  2 +
 Lake/Build.lean           |  4 --
 Lake/BuildTarget.lean     | 80 +++++++++++++++++++++++++++++++++++++--
 Lake/BuildTargets.lean    | 23 +++++++++++
 Lake/BuildTrace.lean      |  7 +++-
 Lake/Package.lean         |  2 +-
 examples/ffi/package.lean | 18 ++++-----
 7 files changed, 116 insertions(+), 20 deletions(-)
 create mode 100644 Lake/BuildTargets.lean

diff --git a/Lake.lean b/Lake.lean
index 3fed7cb58a..ecea28fb1a 100644
--- a/Lake.lean
+++ b/Lake.lean
@@ -5,6 +5,8 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Cli
 import Lake.SearchPath
+-- API file not imported elsewhere; imported here to force build
+import Lake.BuildTargets
 
 def main (args : List String) : IO UInt32 := do
   try
diff --git a/Lake/Build.lean b/Lake/Build.lean
index 06125728ca..7e958258e0 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -70,10 +70,6 @@ def checkIfSameHash (hash : Hash) (file : FilePath) : IO Bool :=
   catch _ =>
     false
 
-/-- 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 build task if the given condition holds, otherwise perform `build`. -/
 def skipIf [Pure m] (cond : Bool) (build : m BuildTask) : m BuildTask := do
   if cond then pure BuildTask.nop else build
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 69a42852af..d3c3330fcb 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lake.BuildTask
 import Lake.BuildTrace
 
+open System
 namespace Lake
 
 --------------------------------------------------------------------------------
@@ -37,6 +38,15 @@ def discardArtifact (self : Target t m α) : Target t m PUnit :=
 def mtime (self : Target MTime m a) : MTime :=
   self.trace
 
+def file (self : Target t m FilePath) : FilePath :=
+  self.artifact
+
+def filesList (self : Target t m (List FilePath)) : List FilePath :=
+  self.artifact
+
+def filesArray (self : Target t m (Array FilePath)) : Array FilePath :=
+  self.artifact
+
 end Target
 
 --------------------------------------------------------------------------------
@@ -106,15 +116,26 @@ def spawn (self : BuildTarget t a) : IO (ActiveBuildTarget t a) := do
 def materialize (self : BuildTarget t a) : IO PUnit :=
   self.task
 
+-- ### Combinators
+
+def after (target : BuildTarget t a) (act : IO PUnit)  : IO PUnit :=
+  target.task *> act
+
+def afterList (targets : List (BuildTarget t a)) (act : IO PUnit) : IO PUnit :=
+  targets.forM (·.task) *> act
+
+instance : HAndThen (BuildTarget t a) (IO PUnit) (IO PUnit) :=
+  ⟨BuildTarget.after⟩
+
+instance : HAndThen (List (BuildTarget t a)) (IO PUnit) (IO PUnit) :=
+  ⟨BuildTarget.afterList⟩
+
 end BuildTarget
 
 --------------------------------------------------------------------------------
 -- # File Targets
 --------------------------------------------------------------------------------
 
-section
-open System
-
 -- ## File Target
 
 abbrev FileTarget :=
@@ -125,11 +146,57 @@ namespace FileTarget
 def mk (file : FilePath) (depMTime : MTime) (task : IO PUnit) : FileTarget :=
   ⟨file, depMTime, task⟩
 
+def compute (file : FilePath) : IO FileTarget := do
+  BuildTarget.pure file (← getMTime file)
+
 protected def pure (file : FilePath) (depMTime : MTime) : FileTarget :=
   BuildTarget.pure file depMTime
 
 end FileTarget
 
+-- ## Files Target
+
+abbrev FilesTarget :=
+  BuildTarget MTime (Array FilePath)
+
+namespace FilesTarget
+
+def files (self : FilesTarget) : Array FilePath :=
+  self.artifact
+
+def filesAsList (self : FilesTarget) : List FilePath :=
+  self.artifact.toList
+
+def filesAsArray (self : FilesTarget) : Array FilePath :=
+  self.artifact
+
+def compute (files : Array FilePath) : IO FilesTarget := do
+  BuildTarget.pure files (MTime.arrayMax <| ← files.mapM getMTime)
+
+def singleton (target : FileTarget) : FilesTarget :=
+  {target with artifact := #[target.file]}
+
+def collectList (targets : List FileTarget) : FilesTarget :=
+  let files := Array.mk <| targets.map (·.file)
+  let mtime := MTime.listMax <| targets.map (·.mtime)
+  BuildTarget.mk files mtime do
+   (← targets.mapM (IOTask.spawn ·.task)).forM (·.await)
+
+def collectArray (targets : Array FileTarget) : FilesTarget :=
+  let files := targets.map (·.file)
+  let mtime := MTime.arrayMax <| targets.map (·.mtime)
+  BuildTarget.mk files mtime do
+   (← targets.mapM (IOTask.spawn ·.task)).forM (·.await)
+
+def collect (targets : Array FileTarget) : FilesTarget :=
+  collectArray targets
+
+end FilesTarget
+
+instance : Coe FileTarget FilesTarget := ⟨FilesTarget.singleton⟩
+instance : Coe (List FileTarget) FilesTarget := ⟨FilesTarget.collectList⟩
+instance : Coe (Array FileTarget) FilesTarget := ⟨FilesTarget.collectArray⟩
+
 -- ## Active File Target
 
 abbrev ActiveFileTarget :=
@@ -144,7 +211,6 @@ protected def pure (file : FilePath) (depMTime : MTime) : ActiveFileTarget :=
   ActiveBuildTarget.pure file depMTime
 
 end ActiveFileTarget
-end
 
 --------------------------------------------------------------------------------
 -- # Lean Target
@@ -155,6 +221,9 @@ abbrev LeanTarget a :=
 
 namespace LeanTarget
 
+def nil : LeanTarget PUnit :=
+  ActiveBuildTarget.pure () Inhabited.default
+
 def hash (self : LeanTarget a) := self.trace.hash
 def mtime (self : LeanTarget a) := self.trace.mtime
 
@@ -167,4 +236,7 @@ def all (targets : List (LeanTarget a)) : IO (LeanTarget PUnit) := do
 def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LeanTarget a :=
   {target with trace := LeanTrace.fromMTime target.trace}
 
+def buildOpaqueFromFileTarget (target : FileTarget) : IO (LeanTarget PUnit) := do
+  LeanTarget.fromMTimeTarget <| ← BuildTarget.spawn target.discardArtifact
+
 end LeanTarget
diff --git a/Lake/BuildTargets.lean b/Lake/BuildTargets.lean
new file mode 100644
index 0000000000..6f7bfec4f8
--- /dev/null
+++ b/Lake/BuildTargets.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Compile
+import Lake.BuildTarget
+
+open System
+namespace Lake
+
+def oFileTarget
+(oFile : FilePath) (srcTarget : FileTarget)
+(args : Array String := #[]) (cmd := "c++") : FileTarget :=
+  FileTarget.mk oFile srcTarget.trace <|
+    unless (← checkIfNewer oFile srcTarget.mtime) do
+      srcTarget >> compileO oFile srcTarget.artifact args (cmd := "c++")
+
+def staticLibTarget
+(libFile : FilePath) (oFilesTarget : FilesTarget) : FileTarget :=
+  FileTarget.mk libFile oFilesTarget.trace do
+    unless (← checkIfNewer libFile oFilesTarget.mtime) do
+      oFilesTarget >> compileStaticLib libFile oFilesTarget.filesAsArray
diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean
index 7aa9b9523b..0b0d86b9ee 100644
--- a/Lake/BuildTrace.lean
+++ b/Lake/BuildTrace.lean
@@ -32,7 +32,8 @@ instance : Ord MTime := inferInstanceAs (Ord SystemTime)
 instance : LT MTime := ltOfOrd
 instance : LE MTime := leOfOrd
 
-def MTime.listMax (mtimes : List MTime) := mtimes.maximum?.getD 0
+def MTime.listMax (mtimes : List MTime) := mtimes.foldl max 0
+def MTime.arrayMax (mtimes : Array MTime) := mtimes.foldl max 0
 
 class GetMTime (α) where
   getMTime : α → IO MTime
@@ -42,6 +43,10 @@ export GetMTime (getMTime)
 instance : GetMTime System.FilePath where
   getMTime file := do (← file.metadata).modified
 
+/-- 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
+
 -- # Combined Trace
 
 structure LeanTrace where
diff --git a/Lake/Package.lean b/Lake/Package.lean
index d20ad34629..6238fefd3b 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -51,7 +51,7 @@ structure PackageConfig where
   libName : String := moduleRoot.toString (escape := false)
   depsDir : FilePath := defaultDepsDir
   dependencies : List Dependency := []
-  buildMoreDepsTarget : IO (ActiveBuildTarget LeanTrace PUnit) := ActiveBuildTarget.nil
+  buildMoreDepsTarget : IO (LeanTarget PUnit) := LeanTarget.nil
   scripts : HashMap String Script := HashMap.empty
   deriving Inhabited
 
diff --git a/examples/ffi/package.lean b/examples/ffi/package.lean
index c8f7931025..df33816062 100644
--- a/examples/ffi/package.lean
+++ b/examples/ffi/package.lean
@@ -1,5 +1,6 @@
-import Lake.Build
 import Lake.Package
+import Lake.BuildTargets
+
 open Lake System
 
 def cDir : FilePath := "c"
@@ -9,14 +10,11 @@ def buildDir := defaultBuildDir
 def addO := buildDir / cDir / "add.o"
 def cLib := buildDir / cDir / "libadd.a"
 
-def fetchAddOTarget : IO ActiveFileTarget := do
-  skipIfNewer addO (← getMTime addSrc) <|
-    BuildTask.spawn <| compileO addO addSrc (cmd := "c++")
+def computeAddOTarget : IO FileTarget := do
+  oFileTarget addO <| ← FileTarget.compute addSrc
 
-def fetchCLibTarget : IO ActiveFileTarget := do
-  let oTarget ← fetchAddOTarget
-  skipIfNewer cLib oTarget.mtime <|
-    oTarget >> compileStaticLib cLib #[addO]
+def computeCLibTarget : IO FileTarget := do
+  staticLibTarget cLib <| ← computeAddOTarget
 
 def package : PackageConfig := {
   name := "ffi"
@@ -28,6 +26,6 @@ def package : PackageConfig := {
   -- specify path to the lib for linker
   linkArgs := #[cLib.toString]
   -- specify the lib target as an additional dependency
-  buildMoreDepsTarget := fetchCLibTarget.map fun target =>
-    LeanTarget.fromMTimeTarget <| target.discardArtifact
+  buildMoreDepsTarget := do
+    LeanTarget.buildOpaqueFromFileTarget <| ← computeCLibTarget
 }