refactor: cleanup/improve Target utils

Lake/Build/Module.lean

@@ -82,8 +82,8 @@ abbrev cTarget (self : ActiveOleanAndCTarget) := self.info.cTarget
 
 end ActiveOleanAndCTarget
 
-def OleanAndCTarget.run' (self : OleanAndCTarget) : BuildM ActiveOleanAndCTarget := do
-  let t ← self.run
+def OleanAndCTarget.activate (self : OleanAndCTarget) : BuildM ActiveOleanAndCTarget := do
+  let t ← Target.activate self
   let oleanTask ← t.mapAsync fun info depTrace => do
     return mixTrace (← computeTrace info.oleanFile) depTrace
   let cTask ← t.mapAsync fun info _ => do
@@ -174,7 +174,7 @@ def recBuildModuleOleanAndCTargetWithLocalImports
   recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
     let importTarget ← ActiveTarget.collectOpaqueList <| importTargets.map (·.oleanTarget)
     let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.run'
+    pkg.moduleOleanAndCTargetOnly mod leanFile contents allDepsTarget |>.activate
 
 def recBuildModuleOleanTargetWithLocalImports
 [Monad m] [MonadLiftT BuildM m] [MonadFunctorT BuildM m] (depTarget : ActiveBuildTarget x)
@@ -182,7 +182,7 @@ def recBuildModuleOleanTargetWithLocalImports
   recBuildModuleWithLocalImports fun pkg mod leanFile contents importTargets => do
     let importTarget ← ActiveTarget.collectOpaqueList importTargets
     let allDepsTarget := Target.active <| ← depTarget.mixOpaqueAsync importTarget
-    pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.run
+    pkg.moduleOleanTargetOnly mod leanFile contents allDepsTarget |>.activate
 
 -- ## Definitions
 

Lake/Build/Package.lean

@@ -18,7 +18,7 @@ namespace Lake
 /-- Build the `extraDepTarget` of all dependent packages into a single target. -/
 protected def Package.buildExtraDepsTarget (self : Package) : BuildM ActiveOpaqueTarget := do
   let collect pkg depTargets := do
-    let extraDepTarget ← self.extraDepTarget.run
+    let extraDepTarget ← self.extraDepTarget.activate
     let depTarget ← ActiveTarget.collectOpaqueArray depTargets
     extraDepTarget.mixOpaqueAsync depTarget
   let build dep recurse := do
@@ -32,7 +32,7 @@ protected def Package.buildExtraDepsTarget (self : Package) : BuildM ActiveOpaqu
 /-- Build the `extraDepTarget` of all workspace packages into a single target. -/
 def buildExtraDepsTarget : BuildM ActiveOpaqueTarget := do
   ActiveTarget.collectOpaqueArray <| ← do
-    (← getWorkspace).packageArray.mapM (·.extraDepTarget.run)
+    (← getWorkspace).packageArray.mapM (·.extraDepTarget.activate)
 
 -- # Build Package Modules
 
@@ -121,15 +121,15 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
   let depTarget ← self.buildExtraDepsTarget
   if imports.isEmpty then
     -- wait for deps to finish building
-    depTarget.build
+    depTarget.buildOpaque
   else
     -- build local imports from list
     let infos := (← getWorkspace).processImportList imports
     if self.defaultFacet == PackageFacet.oleans then
       let build := recBuildModuleOleanTargetWithLocalImports depTarget
       let targets ← buildModuleArray infos build
-      targets.forM (·.build)
+      targets.forM (·.buildOpaque)
     else
       let build := recBuildModuleOleanAndCTargetWithLocalImports depTarget
       let targets ← buildModuleArray infos build
-      targets.forM (·.build)
+      targets.forM (·.buildOpaque)

Lake/Build/Target.lean

@@ -52,13 +52,13 @@ protected def bindAsync [BindAsync n k] [MonadLiftT n m] (self : ActiveTarget i
 protected def bindOpaqueAsync [BindAsync n k] [MonadLiftT n m] (self : ActiveTarget i k α) (f : α → n (k β)) : m (k β) :=
   liftM <| bindAsync self.task f
 
-def materializeAsync [Pure m] (self : ActiveTarget i k t) : m (k t) :=
-  pure self.task
-
 def materialize [Await k m'] [MonadLiftT m' m] (self : ActiveTarget i k t) : m t :=
   liftM <| await self.task
 
-def build [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m PUnit :=
+def build [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m i :=
+  Functor.mapConst self.info self.materialize
+
+def buildOpaque [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m PUnit :=
   discard <| self.materialize
 
 def mixOpaqueAsync
@@ -117,6 +117,12 @@ def withTask (task : m' (k' t')) (self : Target i m k t) : Target i m' k' t' :=
 def opaque (task : m (k t)) : Target PUnit m k t :=
   mk () task
 
+def opaqueAsync [Async m n k] [MonadLiftT n n'] (act : m t) : Target PUnit n' k t :=
+  mk () (liftM <| async act)
+
+protected def async [Async m n k] [MonadLiftT n n'] (info : i) (act : m t) : Target i n' k t :=
+  mk info (liftM <| async act)
+
 def active [Pure m] (target : ActiveTarget i k t) : Target i m k t :=
   mk target.info <| pure target.task
 
@@ -132,9 +138,27 @@ def computeSync [ComputeTrace i m' t] [MonadLiftT m' m] [Functor m] [Pure k] (in
 def computeAsync [ComputeTrace i m' t] [MonadLiftT m' m] [Async m n k] [MonadLiftT n m]  (info : i) : Target i m k t :=
   mk info <| liftM <| async <| liftM (n := m) <| ComputeTrace.computeTrace info
 
-def run [Monad m] (self : Target i m k t) : m (ActiveTarget i k t) :=
+def activate [Functor m] (self : Target i m k t) : m (ActiveTarget i k t) :=
   Functor.map (fun t => ActiveTarget.mk self.info t) self.task
 
+def materializeAsync (self : Target i m k t) : m (k t) :=
+  self.task
+
+def materialize [Await k n] [MonadLiftT n m] [Bind m] (self : Target i m k t) : m t := do
+  self.task >>= (liftM ∘ await)
+
+def build  [Await k n] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i m k t) : m i := do
+  Functor.mapConst self.info self.materialize
+
+def buildOpaque  [Await k n] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i m k t) : m PUnit := do
+  discard self.materialize
+
+def buildAsync [Functor m] [Functor k] (self : Target i m k t) : m (k i) :=
+  Functor.mapConst self.info <$> self.task
+
+def buildOpaqueAsync [Functor m] [Functor k] (self : Target i m k t) : m (k PUnit) :=
+  discard <$> self.task
+
 protected def mapAsync [BindAsync' m n k] [MonadLiftT n m] [Bind m] (self : Target i m k α) (f : i → α → m β) : m (k β) :=
   self.task >>= fun tk => liftM <| bindAsync' tk (f self.info)
 
@@ -147,15 +171,6 @@ protected def bindAsync [BindAsync n k] [MonadLiftT n m] [Bind m] (self : Target
 protected def bindOpaqueAsync [BindAsync n k] [MonadLiftT n m] [Bind m] (self : Target i m k α) (f : α → n (k β)) : m (k β) :=
   self.task >>= fun tk => liftM <| bindAsync tk f
 
-def materializeAsync (self : Target i m k t) : m (k t) :=
-  self.task
-
-def materialize [Await k n] [MonadLiftT n m] [Bind m] (self : Target i m k t) : m t := do
-  self.task >>= (liftM ∘ await)
-
-def build  [Await k n] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i m k t) : m i := do
-  Functor.mapConst self.info self.materialize
-
 def mixOpaqueAsync
 [MixTrace t] [SeqMapAsync n k] [MonadLiftT n m] [Monad m]
 (t1 :  Target α m k t) (t2 :  Target β m k t) : Target PUnit m k t :=

Lake/Build/TargetTypes.lean

@@ -40,6 +40,12 @@ abbrev ActiveFileTarget := ActiveBuildTarget FilePath
 /-- A `BuildTarget` with no artifact information. -/
 abbrev OpaqueTarget := BuildTarget PUnit
 
+@[inline] def OpaqueTarget.mk (act : BuildM (BuildTask BuildTrace)) : OpaqueTarget :=
+  Target.opaque act
+
+@[inline] def OpaqueTarget.async (act : BuildM BuildTrace) : OpaqueTarget :=
+  Target.opaqueAsync act
+
 -- ## Active
 
 /-- An `ActiveBuildTarget` with no artifact information. -/