feat: replace extraDepTarget with extraDepTargets

Lake/Build/Data.lean

@@ -80,6 +80,11 @@ abbrev BuildData : BuildKey → Type
 | .targetFacet _ _ f => TargetData f
 | .customTarget p t => CustomData (p, t)
 
+instance : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
+instance : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
+instance : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
+instance : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
+
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/
 --------------------------------------------------------------------------------

Lake/Build/Index.lean

@@ -27,10 +27,7 @@ dynamically typed equivalent.
   cast (by rw [← h.family_key_eq_type]) build
 
 def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
-  if let some target := lib.pkg.findTargetConfig? (.str lib.name "static") then
-    lib.config.getJob <$> (target.build lib.pkg)
-  else
-    error "missing target for external library"
+  lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
 
 def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
   buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs

Lake/Build/Info.lean

@@ -126,7 +126,7 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 /-- The monad for build functions that are part of the index. -/
 abbrev IndexBuildM := IndexT RecBuildM
 
-/-- Build the given info using the Lake build index. -/
+/-- Fetch the given info using the Lake build index. -/
 @[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexBuildM α :=
   fun build => cast (by simp) <| build self
 

Lake/Build/Job.lean

@@ -62,6 +62,12 @@ namespace BuildJob
 
 instance : Pure BuildJob := ⟨BuildJob.pure⟩
 
+@[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
+  mk <| (fun (a,t) => (f a,t)) <$> self.toJob
+
+instance : Functor BuildJob where
+  map := BuildJob.map
+
 @[inline] protected def bindSync
 (self : BuildJob α) (f : α → BuildTrace → JobM β) : SchedulerM (Job β) :=
   self.toJob.bindSync fun (a, t) => f a t

Lake/Build/Package.lean

@@ -32,15 +32,20 @@ Build the `extraDepTarget` for the package and its transitive dependencies.
 Also fetch pre-built releases for the package's' dependencies.
 -/
 def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do
-  let job ← self.deps.foldlM (do ·.mix <| ← ·.extraDep.fetch) BuildJob.nil
-  -- Fetch dependency's pre-built release if desired
-  let isDepPkg := self.name ≠ (← getWorkspace).root.name
-  let job ← do
-    if isDepPkg ∧ self.preferReleaseBuild then
-      job.mix <| ← self.release.fetch
+  let mut job := BuildJob.nil
+  -- Build dependencies' extra dep targets
+  for dep in self.deps do
+    job ← job.mix <| ← dep.extraDep.fetch
+  -- Fetch pre-built release if desired and this package is a dependency
+  if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
+    job ← job.mix <| ← self.release.fetch
+  -- Build this package's extra dep targets
+  for target in self.extraDepTargets do
+    if let some config := self.findTargetConfig? target then
+      job ← job.mix <| config.getJob <| ← fetch <| self.target target
     else
-      return job
-  job.mix <| ← self.extraDepTarget
+      error s!"unknown target `{target}`"
+  return job
 
 /-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
 def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=

Lake/CLI/Build.lean

@@ -84,10 +84,8 @@ def resolveCustomTarget (pkg : Package)
     throw <| CliError.invalidFacet name facet
   else do
     let info := pkg.target name
-    let some getJob := config.getJob?
-      | throw <| CliError.nonCliTarget name
     have h : BuildData info.key = CustomData (pkg.name, name) := rfl
-    return {info, getJob := h ▸ getJob}
+    return {info, getJob := fun data => discard (h ▸ config.getJob data).toJob}
 
 def resolveTargetInPackage (ws : Workspace)
 (pkg : Package) (target facet : Name) : Except CliError BuildSpec :=

Lake/Config/ExternLib.lean

@@ -33,3 +33,7 @@ That is, the package's `moreLinkArgs`.
 -/
 @[inline] def linkArgs (self : ExternLib) : Array String :=
   self.pkg.moreLinkArgs
+
+/-- The name of the package target used to build the external library's static binary. -/
+@[inline] def staticTargetName (self : ExternLib) : Name :=
+  .str self.name "static"

Lake/Config/Package.lean

@@ -70,15 +70,8 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   /-- The `Name` of the package. -/
   name : Name
 
-  /--
-  An extra `OpaqueTarget` that should be built before the package.
-
-  `OpaqueTarget.collectList/collectArray` can be used combine multiple
-  extra targets into a single `extraDepTarget`.
-
-  **DEPRECATED:** Use separate custom `target` declarations instead?
-  -/
-  extraDepTarget : Option (SchedulerM (BuildJob Unit)) := none
+  /-- An `Array` of target names to build whenever the package is used. -/
+  extraDepTargets : Array Name := #[]
 
   /--
   Whether to compile each of the package's module into a native shared library
@@ -234,9 +227,9 @@ def manifestFile (self : Package) : FilePath :=
 @[inline] def buildDir (self : Package) : FilePath :=
   self.dir / self.config.buildDir
 
-/-- The package's `extraDepTarget` configuration. -/
-@[inline] def extraDepTarget (self : Package) : SchedulerM (BuildJob Unit) :=
-  self.config.extraDepTarget.getD (pure BuildJob.nil)
+/-- The package's `extraDepTargets` configuration. -/
+@[inline] def extraDepTargets (self : Package) : Array Name :=
+  self.config.extraDepTargets
 
 /-- The package's `releaseRepo?` configuration. -/
 @[inline] def releaseRepo? (self : Package) : Option String :=

Lake/Config/TargetConfig.lean

@@ -13,16 +13,16 @@ structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
   build : (pkg : Package) → [Fact (pkg.name = pkgName)] →
     IndexBuildM (CustomData (pkgName, name))
-  /-- Does this target produce an associated asynchronous job? -/
-  getJob? : Option (CustomData (pkgName, name) → Job Unit)
+  /-- The target's resulting build job. -/
+  getJob : CustomData (pkgName, name) → BuildJob Unit
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
 (build : (pkg : Package) → [Fact (pkg.name = pkgName)] → IndexBuildM (BuildJob α))
 [h : FamilyDef CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
   build := cast (by rw [← h.family_key_eq_type]) build
-  getJob? := some fun data => discard <| ofFamily data
+  getJob := fun data => discard <| ofFamily data
 
 /-- A dependently typed configuration based on its registered package and name. -/
 structure TargetDecl where