refactor: generalize module facet build code to any target

leanprover · Jun 23, 2022 · f4c604b · f4c604b
1 parent 23938ed
commit f4c604b
Show file tree

Hide file tree

Showing 8 changed files with 477 additions and 233 deletions.
diff --git a/Lake/Build/Binary.lean b/Lake/Build/Binary.lean
@@ -19,10 +19,9 @@ def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Packag
 def Package.mkStaticLibTarget (lib : LeanLibConfig) (self : Package) : FileTarget :=
   let libFile := self.libDir / lib.staticLibFileName
   BuildTarget.mk' libFile do
-    withExtraDepTarget (← self.buildExtraDepsTarget) do
-      let mods ← self.getLibModuleArray lib
-      let oFileTargets := self.localTargetsOf <| ← buildModuleMap mods &`lean.o
-      staticLibTarget libFile oFileTargets |>.materializeAsync
+    let mods ← self.getLibModuleArray lib
+    let oFileTargets := self.localTargetsOf <| ← buildModuleFacetMap mods &`lean.o
+    staticLibTarget libFile oFileTargets |>.materializeAsync
 
 protected def Package.staticLibTarget (self : Package) : FileTarget :=
   self.mkStaticLibTarget self.builtinLibConfig
@@ -46,11 +45,10 @@ def Package.linkTargetsOf
 def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarget :=
   let libFile := self.libDir / lib.sharedLibFileName
   BuildTarget.mk' libFile do
-    withExtraDepTarget (← self.buildExtraDepsTarget) do
-      let mods ← self.getLibModuleArray lib
-      let linkTargets ← self.linkTargetsOf <| ← buildModuleMap mods &`lean.o
-      let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
-      target.materializeAsync
+    let mods ← self.getLibModuleArray lib
+    let linkTargets ← self.linkTargetsOf <| ← buildModuleFacetMap mods &`lean.o
+    let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
+    target.materializeAsync
 
 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
   self.mkSharedLibTarget self.builtinLibConfig
@@ -61,18 +59,17 @@ def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
   let exeFile := self.binDir / exe.fileName
   BuildTarget.mk' exeFile do
     let root : Module := ⟨self, WfName.ofName exe.root⟩
-    withExtraDepTarget (← self.buildExtraDepsTarget) do
-      let cTargetMap ← buildModuleMap #[root] &`lean.c
-      let pkgLinkTargets ← self.linkTargetsOf cTargetMap
-      let linkTargets :=
-        if self.isLocalModule exe.root then
-          pkgLinkTargets
-        else
-          let rootTarget := cTargetMap.find? root.name |>.get!
-          let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
-          #[rootLinkTarget] ++ pkgLinkTargets
-      let target := leanExeTarget exeFile linkTargets exe.linkArgs
-      target.materializeAsync
+    let cTargetMap ← buildModuleFacetMap #[root] &`lean.c
+    let pkgLinkTargets ← self.linkTargetsOf cTargetMap
+    let linkTargets :=
+      if self.isLocalModule exe.root then
+        pkgLinkTargets
+      else
+        let rootTarget := cTargetMap.find? root.name |>.get!
+        let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
+        #[rootLinkTarget] ++ pkgLinkTargets
+    let target := leanExeTarget exeFile linkTargets exe.linkArgs
+    target.materializeAsync
 
 protected def Package.exeTarget (self : Package) : FileTarget :=
   self.mkExeTarget self.builtinExeConfig
diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean
@@ -22,7 +22,6 @@ abbrev Job := BuildTask BuildTrace
 /-- A Lake context with some additional caching for builds. -/
 structure BuildContext extends Context where
   leanTrace : BuildTrace
-  extraDepJob : Job := pure nilTrace
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext