From 3e1cdda87e1081ef070f35be0cf02a8662af6313 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 4 Sep 2021 18:53:21 -0400
Subject: [PATCH] refactor: make `PackageConfig` take normal targets

---
 Lake/BuildBin.lean        |  4 ++--
 Lake/BuildPackage.lean    |  2 +-
 Lake/Package.lean         | 12 ++++++------
 examples/ffi/package.lean |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean
index 6c479e7e45..11bfcf9a00 100644
--- a/Lake/BuildBin.lean
+++ b/Lake/BuildBin.lean
@@ -45,7 +45,7 @@ def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : BuildM ActiveFil
     compileStaticLib self.package.staticLibFile oFiles
 
 def PackageTarget.fetchStaticLibTargets (self : PackageTarget) : BuildM (Array ActiveFileTarget) := do
-  #[← self.fetchStaticLibTarget] ++ (← self.package.buildMoreLibTargets)
+  #[← self.fetchStaticLibTarget] ++ (← self.package.moreLibTargets.mapM (·.run))
 
 def Package.fetchStaticLibTarget (self : Package) : BuildM ActiveFileTarget := do
   (← self.buildTarget).fetchStaticLibTarget
@@ -65,7 +65,7 @@ def PackageTarget.fetchBinTarget
   let oFileTargets ← self.fetchOFileTargets
   let depLibTargets ← depTargets.foldlM
     (fun ts dep => do pure <| ts ++ (← dep.fetchStaticLibTargets)) #[]
-  let moreLibTargets ← self.package.buildMoreLibTargets
+  let moreLibTargets ← self.package.moreLibTargets.mapM (·.run)
   let linkTargets := oFileTargets ++ depLibTargets ++ moreLibTargets
   let linksTarget ← ActiveTarget.collectArray linkTargets
   skipIfNewer self.package.binFile linksTarget fun links =>
diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean
index 4b0583795c..211f0261b6 100644
--- a/Lake/BuildPackage.lean
+++ b/Lake/BuildPackage.lean
@@ -82,7 +82,7 @@ def Package.buildRootOleanTarget
 
 def Package.buildDepTargetWith
 (depTargets : List PackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do
-  let extraDepTarget ← self.buildExtraDepTarget
+  let extraDepTarget ← self.extraDepTarget.run
   let depTarget ← ActiveTarget.collectOpaqueList depTargets
   extraDepTarget.mixOpaqueAsync depTarget
 
diff --git a/Lake/Package.lean b/Lake/Package.lean
index a7925f2c73..b5d4091549 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -49,10 +49,10 @@ structure PackageConfig where
   binName : String := name
   libDir : FilePath := defaultLibDir
   libName : String := moduleRoot.toString (escape := false)
-  buildMoreLibTargets : BuildM (Array ActiveFileTarget) := #[]
+  moreLibTargets : Array FileTarget := #[]
   depsDir : FilePath := defaultDepsDir
   dependencies : List Dependency := []
-  buildExtraDepTarget : BuildM ActiveOpaqueTarget := ActiveTarget.nil
+  extraDepTarget : OpaqueTarget := Target.nil
   scripts : HashMap String Script := HashMap.empty
   deriving Inhabited
 
@@ -86,8 +86,8 @@ def moduleRootName (self : Package) : String :=
 def dependencies (self : Package) : List Dependency :=
   self.config.dependencies
 
-def buildExtraDepTarget (self : Package) : BuildM ActiveOpaqueTarget :=
-  self.config.buildExtraDepTarget
+def extraDepTarget (self : Package) : OpaqueTarget :=
+  self.config.extraDepTarget
 
 def leanArgs (self : Package) : Array String :=
   self.config.leanArgs
@@ -167,5 +167,5 @@ def staticLibFileName (self : Package) : FilePath :=
 def staticLibFile (self : Package) : FilePath :=
   self.libDir / self.staticLibFileName
 
-def buildMoreLibTargets (self : Package) : BuildM (Array ActiveFileTarget) :=
-  self.config.buildMoreLibTargets
+def moreLibTargets (self : Package) : Array FileTarget :=
+  self.config.moreLibTargets
diff --git a/examples/ffi/package.lean b/examples/ffi/package.lean
index b646436217..36b6120724 100644
--- a/examples/ffi/package.lean
+++ b/examples/ffi/package.lean
@@ -24,5 +24,5 @@ def package : PackageConfig := {
   moduleRoot := `Add
   binName := "add"
   -- specify the lib as an additional target
-  buildMoreLibTargets := do #[← cLibTarget.run]
+  moreLibTargets := #[cLibTarget]
 }