feat: user-specified native module facets for libraries
This commit is contained in:
tydeu
parent
85f6d1a402
commit
f62b017654
8 changed files with 192 additions and 94 deletions
|
|
@ -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
|
||||
|
|
|
|||
89
Lake/Build/Facets.lean
Normal file
89
Lake/Build/Facets.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue