diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean index 909e73048a..962e3d699f 100644 --- a/Lake/Build/Data.lean +++ b/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 -/ -------------------------------------------------------------------------------- diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 392ef8a051..596a492739 100644 --- a/Lake/Build/Index.lean +++ b/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 diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index f43260719f..b2b1d82662 100644 --- a/Lake/Build/Info.lean +++ b/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 diff --git a/Lake/Build/Job.lean b/Lake/Build/Job.lean index 99d6a53fda..11c75be7c2 100644 --- a/Lake/Build/Job.lean +++ b/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 diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index 3f49655d24..a5164ffcc6 100644 --- a/Lake/Build/Package.lean +++ b/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 := diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 9cab7c7de8..e040c09e25 100644 --- a/Lake/CLI/Build.lean +++ b/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 := diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean index 1378f02512..77b2043727 100644 --- a/Lake/Config/ExternLib.lean +++ b/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" diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 2f78c70698..76151b8aa0 100644 --- a/Lake/Config/Package.lean +++ b/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 := diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean index a839b1b668..c22a9f6bb9 100644 --- a/Lake/Config/TargetConfig.lean +++ b/Lake/Config/TargetConfig.lean @@ -13,8 +13,8 @@ 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. -/ @@ -22,7 +22,7 @@ structure TargetConfig (pkgName name : Name) : Type where (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