From f62b0176546c61c73c1931f3f8dd37588153fad1 Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 29 Jun 2022 03:36:05 -0400 Subject: [PATCH] feat: user-specified native module facets for libraries --- Lake/Build/Data.lean | 12 +++ Lake/Build/Facets.lean | 89 +++++++++++++++++++++ Lake/Build/Info.lean | 139 ++++++++++++++------------------- Lake/Build/Module.lean | 12 +-- Lake/Build/Roots.lean | 17 ++-- Lake/Config/LeanLib.lean | 4 + Lake/Config/LeanLibConfig.lean | 10 ++- Lake/Config/Module.lean | 3 + 8 files changed, 192 insertions(+), 94 deletions(-) create mode 100644 Lake/Build/Facets.lean diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean index 2d0db0a5f8..4fb462e224 100644 --- a/Lake/Build/Data.lean +++ b/Lake/Build/Data.lean @@ -9,6 +9,10 @@ import Lake.Util.DynamicType open Lean namespace Lake +-------------------------------------------------------------------------------- +/-! ## Build Data Subtypes -/ +-------------------------------------------------------------------------------- + /-- Type of build data associated with a module facet in the Lake build store. For example a transitive × direct import pair for `imports` or an active build @@ -25,6 +29,10 @@ opaque PackageData (facet : WfName) : Type /-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/ opaque TargetData (facet : WfName) : Type +-------------------------------------------------------------------------------- +/-! ## Build Data -/ +-------------------------------------------------------------------------------- + /-- Type of the build data associated with a key in the Lake build store. It is dynamic type composed of the three separate dynamic types for modules, @@ -65,6 +73,10 @@ theorem isTargetKey_data {k : BuildKey} have ⟨has_p, has_t⟩ := of_decide_eq_true h simp [of_decide_eq_true has_p, of_decide_eq_true has_t, h] +-------------------------------------------------------------------------------- +/-! ## Macros for Declaring Build Data -/ +-------------------------------------------------------------------------------- + /-- Macro for declaring new `PackageData`. -/ scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment) "package_data " id:ident " : " ty:term : command => do diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean new file mode 100644 index 0000000000..29f99221c1 --- /dev/null +++ b/Lake/Build/Facets.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Data +import Lake.Build.TargetTypes + +/-! +# Simple Builtin Facet Declarations + +This module declares most of the builtin facets an targets and +their build data builtin facets and targets. Some of these definitions +are needed for configurations, so we define them here before we need to +import said configurations for `BuildInfo`. +-/ + +namespace Lake + +-- ## Module Facets + +/-- A module facet name along with proof of its data type. -/ +structure ModuleFacet (α) where + /-- The name of the module facet. -/ + name : WfName + /-- Proof that module's facet build result is of type α. -/ + data_eq : ModuleData name = α + deriving Repr + +instance (facet : ModuleFacet α) : DynamicType ModuleData facet.name α := + ⟨facet.data_eq⟩ + +instance [DynamicType ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) := + ⟨facet, eq_dynamic_type⟩ + +namespace Module +abbrev binFacet := &`lean.bin +abbrev oleanFacet := &`olean +abbrev ileanFacet := &`ilean +abbrev cFacet := &`lean.c +abbrev oFacet := &`lean.o +abbrev dynlibFacet := &`lean.dynlib +end Module + +/-- Lean binary build (`olean`, `ilean` files) -/ +module_data lean.bin : ActiveOpaqueTarget + +/-- The `olean` file produced by `lean` -/ +module_data olean : ActiveFileTarget + +/-- The `ilean` file produced by `lean` -/ +module_data ilean : ActiveFileTarget + +/-- The C file built from the Lean file via `lean` -/ +module_data lean.c : ActiveFileTarget + +/-- The object file built from `lean.c` -/ +module_data lean.o : ActiveFileTarget + +/-- Shared library for `--load-dynlib` -/ +module_data lean.dynlib : ActiveFileTarget + +-- ## Package Facets + +/-- The package's `extraDepTarget`. -/ +package_data extraDep : ActiveOpaqueTarget + +-- ## Target Facets + +abbrev LeanLib.staticFacet := &`leanLib.static +abbrev LeanLib.sharedFacet := &`leanLib.shared +abbrev LeanExe.facet := &`leanExe +abbrev ExternLib.staticFacet := &`externLib.static +abbrev ExternLib.sharedFacet := &`externLib.shared + +/-- A Lean library's static binary. -/ +target_data leanLib.static : ActiveFileTarget + +/-- A Lean library's shared binary. -/ +target_data leanLib.shared : ActiveFileTarget + +/-- A Lean binary executable. -/ +target_data leanExe : ActiveFileTarget + +/-- A external library's static binary. -/ +target_data externLib.static : ActiveFileTarget + +/-- A external library's shared binary. -/ +target_data externLib.shared : ActiveFileTarget diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index c59740e901..d3da392935 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -3,14 +3,37 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lake.Build.Data import Lake.Config.LeanExe import Lake.Config.ExternLib +import Lake.Build.Facets import Lake.Util.EquipT +/-! +# Build Info + +This module defines the Lake build info type and related utilities. +Build info is what is the data passed to a Lake build function to facilitate +the build. +-/ + namespace Lake --- # Build Key Helper Constructors +/-- The type of Lake's build info. -/ +inductive BuildInfo +| module (module : Module) (facet : WfName) +| package (package : Package) (facet : WfName) +| staticLeanLib (lib : LeanLib) +| sharedLeanLib (lib : LeanLib) +| leanExe (exe : LeanExe) +| staticExternLib (lib : ExternLib) +| sharedExternLib (lib : ExternLib) +| custom (package : Package) (target : WfName) (facet : WfName) + +-------------------------------------------------------------------------------- +/-! ## Build Info & Keys -/ +-------------------------------------------------------------------------------- + +/-! ### Build Key Helper Constructors -/ abbrev Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet := ⟨⟨none, self.name, facet⟩, rfl, rfl⟩ @@ -18,12 +41,6 @@ abbrev Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet abbrev Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet := ⟨⟨self.name, none, facet⟩, rfl, rfl⟩ -abbrev LeanLib.staticFacet := &`leanLib.static -abbrev LeanLib.sharedFacet := &`leanLib.shared -abbrev LeanExe.facet := &`leanExe -abbrev ExternLib.staticFacet := &`externLib.static -abbrev ExternLib.sharedFacet := &`externLib.shared - abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey := ⟨self.pkg.name, self.name, staticFacet⟩ @@ -39,19 +56,9 @@ abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey := abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey := ⟨self.pkg.name, self.name, sharedFacet⟩ --- # Build Info - -/-- The type of Lake's build info. -/ -inductive BuildInfo -| module (module : Module) (facet : WfName) -| package (package : Package) (facet : WfName) -| staticLeanLib (lib : LeanLib) -| sharedLeanLib (lib : LeanLib) -| leanExe (exe : LeanExe) -| staticExternLib (lib : ExternLib) -| sharedExternLib (lib : ExternLib) -| custom (package : Package) (target : WfName) (facet : WfName) +/-! ### Build Info to Key -/ +/-- The key that identifies the build in the Lake build store. -/ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey | module m f => m.mkBuildKey f | package p f => p.mkBuildKey f @@ -62,7 +69,7 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey | sharedExternLib l => l.sharedBuildKey | custom p t f => ⟨p.name, t, f⟩ --- # Instances for deducing data types of `BuildInfo` keys +/-! ### Instances for deducing data types of `BuildInfo` keys -/ instance [DynamicType ModuleData f α] : DynamicType BuildData (BuildInfo.key (.module m f)) α where @@ -92,7 +99,9 @@ instance [DynamicType TargetData ExternLib.sharedFacet α] : DynamicType BuildData (BuildInfo.key (.sharedExternLib l)) α where eq_dynamic_type := by unfold BuildData; simp [eq_dynamic_type] --- # Recursive Facet Builds +-------------------------------------------------------------------------------- +/-! ## Recursive Building -/ +-------------------------------------------------------------------------------- /-- A build function for any element of the Lake build index. -/ abbrev IndexBuildFn (m : Type → Type v) := @@ -108,7 +117,33 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m export BuildInfo (recBuild) --- # Build Info Helper Constructors +-------------------------------------------------------------------------------- +/-! ## Build Info & Facets -/ +-------------------------------------------------------------------------------- + +/-! +### Complex Builtin Facet Declarations + +Additional builtin build data types on top of those defined in `FacetData` . +Defined here because they need to import configurations, whereas the definitions +there need to be imported by configurations. +-/ + +abbrev Module.importFacet := &`lean.imports + +/-- The direct × transitive imports of the Lean module. -/ +module_data lean.imports : Array Module × Array Module + +/-- The package's complete array of transitive dependencies. -/ +package_data deps : Array Package + + +/-! +### Facet Build Info Helper Constructors + +Definitions to easily construct `BuildInfo` values for module, package, +and target facets. +-/ namespace Module @@ -116,14 +151,6 @@ namespace Module abbrev facet (facet : WfName) (self : Module) : BuildInfo := .module self facet -abbrev importFacet := &`lean.imports -abbrev binFacet := &`lean.bin -abbrev oleanFacet := &`olean -abbrev ileanFacet := &`ilean -abbrev cFacet := &`lean.c -abbrev oFacet := &`lean.o -abbrev dynlibFacet := &`lean.dynlib - variable (self : Module) abbrev imports := self.facet importFacet @@ -163,53 +190,3 @@ abbrev ExternLib.static (self : ExternLib) : BuildInfo := /-- Build info of the external library's shared binary. -/ abbrev ExternLib.shared (self : ExternLib) : BuildInfo := .sharedExternLib self - --- # Data Types of Build Results - --- ## For Module Facets - -/-- Lean binary build (`olean`, `ilean` files) -/ -module_data lean.bin : ActiveOpaqueTarget - -/-- The `olean` file produced by `lean` -/ -module_data olean : ActiveFileTarget - -/-- The `ilean` file produced by `lean` -/ -module_data ilean : ActiveFileTarget - -/-- The C file built from the Lean file via `lean` -/ -module_data lean.c : ActiveFileTarget - -/-- The object file built from `lean.c` -/ -module_data lean.o : ActiveFileTarget - -/-- Shared library for `--load-dynlib` -/ -module_data lean.dynlib : ActiveFileTarget - -/-- The direct × transitive imports of the Lean module. -/ -module_data lean.imports : Array Module × Array Module - --- ## For Package Facets - -/-- The package's complete array of transitive dependencies. -/ -package_data deps : Array Package - -/-- The package's `extraDepTarget`. -/ -package_data extraDep : ActiveOpaqueTarget - --- ## For Target Types - -/-- A Lean library's static binary. -/ -target_data leanLib.static : ActiveFileTarget - -/-- A Lean library's shared binary. -/ -target_data leanLib.shared : ActiveFileTarget - -/-- A Lean binary executable. -/ -target_data leanExe : ActiveFileTarget - -/-- A external library's static binary. -/ -target_data externLib.static : ActiveFileTarget - -/-- A external library's shared binary. -/ -target_data externLib.shared : ActiveFileTarget diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 42f251334a..3e1bc4efa1 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -43,14 +43,15 @@ def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget := leanOFileTarget self.oFile cTarget self.leancArgs @[inline] -def Module.mkDynlibTarget (self : Module) (oTarget : FileTarget) +def Module.mkDynlibTarget (self : Module) (linkTargets : Array FileTarget) (libDirs : Array FilePath) (libTargets : Array FileTarget) : FileTarget := + let linksTarget : BuildTarget _ := Target.collectArray linkTargets let libsTarget : BuildTarget _ := Target.collectArray libTargets Target.mk self.dynlibName do - oTarget.bindAsync fun oFile oTrace => do + linksTarget.bindAsync fun links oTrace => do libsTarget.bindSync fun libFiles libTrace => do buildFileUnlessUpToDate self.dynlibFile (oTrace.mix libTrace) do - let args := #[oFile.toString] ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l{·}") + let args := links.map toString ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l{·}") compileSharedLib self.dynlibFile args (← getLeanc) -- # Recursive Building @@ -156,7 +157,8 @@ Recursively build the shared library of a module (e.g., for `--load-dynlib`). : IndexT m ActiveFileTarget := do have : MonadLift BuildM m := ⟨liftM⟩ let (_, transImports) ← mod.imports.recBuild - let oTarget := Target.active (← mod.o.recBuild) + let linkTargets ← mod.nativeFacets.mapM fun facet => do + return Target.active <| ← recBuild <| mod.facet facet.name let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports let libTargets := modTargets ++ pkgTargets |>.map Target.active - mod.mkDynlibTarget oTarget libDirs libTargets |>.activate + mod.mkDynlibTarget linkTargets libDirs libTargets |>.activate diff --git a/Lake/Build/Roots.lean b/Lake/Build/Roots.lean index 90b4168082..f79ed0d304 100644 --- a/Lake/Build/Roots.lean +++ b/Lake/Build/Roots.lean @@ -14,8 +14,8 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m] -- # Build Static Lib /-- Build and collect the specified facet of the library's local modules. -/ -@[specialize] def LeanLib.recBuildLocalModules (facet : WfName) (self : LeanLib) -[DynamicType ModuleData facet α]: IndexT m (Array α) := do +@[specialize] def LeanLib.recBuildLocalModules +(facets : Array (ModuleFacet α)) (self : LeanLib) : IndexT m (Array α) := do have : MonadLift BuildM m := ⟨liftM⟩ let mut results := #[] let mut modSet := ModuleSet.empty @@ -26,14 +26,15 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m] for mod in mods do if self.isLocalModule mod.name then unless modSet.contains mod do - results := results.push <| ← recBuild <| mod.facet facet + for facet in facets do + results := results.push <| ← recBuild <| mod.facet facet.name modSet := modSet.insert mod return results @[specialize] protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do have : MonadLift BuildM m := ⟨liftM⟩ - let oTargets := (← self.recBuildLocalModules Module.oFacet).map Target.active + let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active staticLibTarget self.staticLibFile oTargets |>.activate -- # Build Shared Lib @@ -43,7 +44,8 @@ Build and collect the local object files and external libraries of a library and its modules' imports. -/ @[specialize] def LeanLib.recBuildLinks -(self : LeanLib) : IndexT m (Array ActiveFileTarget) := do +(facets : Array (ModuleFacet ActiveFileTarget)) (self : LeanLib) +: IndexT m (Array ActiveFileTarget) := do have : MonadLift BuildM m := ⟨liftM⟩ -- Build and collect modules let mut pkgs := #[] @@ -60,7 +62,8 @@ of a library and its modules' imports. pkgSet := pkgSet.insert mod.pkg pkgs := pkgs.push mod.pkg if self.isLocalModule mod.name then - targets := targets.push <| ← mod.o.recBuild + for facet in facets do + targets := targets.push <| ← recBuild <| mod.facet facet.name modSet := modSet.insert mod -- Build and collect external library targets for pkg in pkgs do @@ -72,7 +75,7 @@ of a library and its modules' imports. @[specialize] protected def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarget := do have : MonadLift BuildM m := ⟨liftM⟩ - let linkTargets := (← self.recBuildLinks).map Target.active + let linkTargets := (← self.recBuildLinks self.nativeFacets).map Target.active leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate -- # Build Executable diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean index 8085a6445f..afca1cf398 100644 --- a/Lake/Config/LeanLib.lean +++ b/Lake/Config/LeanLib.lean @@ -69,6 +69,10 @@ Is true if either the package or the library have `precompileModules` set. @[inline] def precompileModules (self : LeanLib) : Bool := self.pkg.precompileModules || self.config.precompileModules +/-- The library's `nativeFacets` configuration. -/ +@[inline] def nativeFacets (self : LeanLib) : Array (ModuleFacet ActiveFileTarget) := + self.config.nativeFacets + /-- The arguments to pass to `lean` when compiling the library's Lean files. That is, the package's `moreLeanArgs` plus the library's `moreLeanArgs`. diff --git a/Lake/Config/LeanLibConfig.lean b/Lake/Config/LeanLibConfig.lean index 6110eb7375..4170f01f11 100644 --- a/Lake/Config/LeanLibConfig.lean +++ b/Lake/Config/LeanLibConfig.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Util.Casing +import Lake.Build.Facets import Lake.Config.InstallPath import Lake.Config.LeanConfig import Lake.Config.Glob @@ -60,7 +61,14 @@ structure LeanLibConfig extends LeanConfig where -/ precompileModules : Bool := false -deriving Inhabited, Repr + /-- + The set of module facets to build and combine into the library's static + and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file + compiled from the Lean source). + -/ + nativeFacets : Array (ModuleFacet ActiveFileTarget) := #[Module.oFacet] + +deriving Inhabited namespace LeanLibConfig diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index efe7e0b34e..fd44073981 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -78,6 +78,9 @@ abbrev pkg (self : Module) : Package := @[inline] def shouldPrecompile (self : Module) : Bool := self.lib.precompileModules +@[inline] def nativeFacets (self : Module) : Array (ModuleFacet ActiveFileTarget) := + self.lib.nativeFacets + @[inline] def isLeanOnly (self : Module) : Bool := self.pkg.isLeanOnly && !self.shouldPrecompile