feat: library facets

Author: tydeu

Diff for: Lake/Build.lean

@@ -8,4 +8,5 @@ import Lake.Build.Actions
 import Lake.Build.Index
 import Lake.Build.Module
 import Lake.Build.Package
+import Lake.Build.Library
 import Lake.Build.Imports

Diff for: Lake/Build/Data.lean

@@ -14,7 +14,7 @@ namespace Lake
 --------------------------------------------------------------------------------
 
 /--
-The open type family which maps a module facet's name to it build data
+The open type family which maps a module facet's name to its build data
 in the Lake build store. For example, a transitive × direct import pair
 for the `lean.imports` facet or an active build target for `lean.c`.
 
@@ -24,7 +24,7 @@ as needed (via `module_data`).
 opaque ModuleData (facet : Name) : Type
 
 /--
-The open type family which maps a package facet's name to it build data
+The open type family which maps a package facet's name to its build data
 in the Lake build store. For example, a transitive dependencies of the package
 for the facet `deps`.
 
@@ -43,6 +43,19 @@ as needed (via `target_data`).
 -/
 opaque TargetData (facet : Name) : Type
 
+/-
+The open type family which maps a library facet's name to its build data
+in the Lake build store. For example, an active build target for the `static`
+facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `library_data`).
+-/
+abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet)
+
+instance [h : FamilyDef TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
+  ⟨h.family_key_eq_type⟩
+
 /--
 The open type family which maps a custom target (package × target name) to
 its build data in the Lake build store.
@@ -85,6 +98,14 @@ scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
   let key := Name.quoteFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
+/-- Macro for declaring new `TargetData` for libraries. -/
+scoped macro (name := libraryDataDecl) doc?:optional(Parser.Command.docComment)
+"library_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``TargetData
+  let key := Name.quoteFrom id id.getId
+  let id := mkIdentFrom id <| id.getId.modifyBase (`leanLib ++ ·)
+  `($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty)
+
 /-- Macro for declaring new `TargetData`. -/
 scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
 "target_data " id:ident " : " ty:term : command => do

Diff for: Lake/Build/Executable.lean

@@ -0,0 +1,26 @@
+/-
+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.Info
+import Lake.Build.Store
+import Lake.Build.Targets
+
+namespace Lake
+
+/-! # Build Executable -/
+
+protected def LeanExe.recBuildExe
+(self : LeanExe) : IndexT RecBuildM ActiveFileTarget := do
+  let (_, imports) ← self.root.imports.recBuild
+  let linkTargets := #[Target.active <| ← self.root.o.recBuild]
+  let mut linkTargets ← imports.foldlM (init := linkTargets) fun arr mod => do
+    let mut arr := arr
+    for facet in mod.nativeFacets do
+      arr := arr.push <| Target.active <| ← recBuild <| mod.facet facet.name
+    return arr
+  let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg
+  for dep in deps do for lib in dep.externLibs do
+    linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
+  leanExeTarget self.file linkTargets self.linkArgs |>.activate

Diff for: Lake/Build/Facets.lean

@@ -71,16 +71,16 @@ package_data extraDep : ActiveOpaqueTarget
 /-! ## Target Facets -/
 
 /-- A Lean library's Lean libraries. -/
-abbrev LeanLib.leanFacet := `leanLib.lean
-target_data leanLib.lean : ActiveOpaqueTarget
+abbrev LeanLib.leanFacet := `lean
+library_data lean : ActiveOpaqueTarget
 
 /-- A Lean library's static binary. -/
-abbrev LeanLib.staticFacet := `leanLib.static
-target_data leanLib.static : ActiveFileTarget
+abbrev LeanLib.staticFacet := `static
+library_data static : ActiveFileTarget
 
 /-- A Lean library's shared binary. -/
-abbrev LeanLib.sharedFacet := `leanLib.shared
-target_data leanLib.shared : ActiveFileTarget
+abbrev LeanLib.sharedFacet := `shared
+library_data shared : ActiveFileTarget
 
 /-- A Lean binary executable. -/
 abbrev LeanExe.exeFacet := `leanExe

Diff for: Lake/Build/Index.lean

@@ -3,7 +3,7 @@ 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.Roots
+import Lake.Build.Executable
 import Lake.Build.Topological
 
 /-!
@@ -51,12 +51,11 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
       error "target's name in the configuration does not match the name it was registered with"
   else
       error s!"could not build `{target}` of `{pkg.name}` -- target not found"
-| .leanLib lib =>
-  mkTargetFacetBuild LeanLib.leanFacet lib.recBuildLean
-| .staticLeanLib lib =>
-  mkTargetFacetBuild LeanLib.staticFacet lib.recBuildStatic
-| .sharedLeanLib lib =>
-  mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared
+| .libraryFacet lib facet => do
+  if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
+    config.build lib
+  else
+    error s!"do not know how to build library facet `{facet}`"
 | .leanExe exe =>
   mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
 | .staticExternLib lib =>
@@ -108,13 +107,11 @@ export BuildInfo (build)
 [FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
   self.facet facet |>.target
 
-/-! ### Pure Lean Lib Targets -/
+/-! ### Lean Library Targets -/
 
 @[inline] protected def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
   self.lean.target
 
-/-! ### Native Lean Lib Targets -/
-
 @[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
   self.static.target.withInfo self.sharedLibFile
 

Diff for: Lake/Build/Info.lean

@@ -22,9 +22,7 @@ namespace Lake
 inductive BuildInfo
 | moduleFacet (module : Module) (facet : Name)
 | packageFacet (package : Package) (facet : Name)
-| leanLib (lib : LeanLib)
-| staticLeanLib (lib : LeanLib)
-| sharedLeanLib (lib : LeanLib)
+| libraryFacet (lib : LeanLib) (facet : Name)
 | leanExe (exe : LeanExe)
 | staticExternLib (lib : ExternLib)
 | sharedExternLib (lib : ExternLib)
@@ -45,14 +43,8 @@ abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
 abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
   .customTarget self.name target
 
-abbrev LeanLib.leanBuildKey (self : LeanLib) : BuildKey :=
-  .targetFacet self.pkg.name self.name leanFacet
-
-abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
-  .targetFacet self.pkg.name self.name staticFacet
-
-abbrev LeanLib.sharedBuildKey (self : LeanLib) : BuildKey :=
-  .targetFacet self.pkg.name self.name sharedFacet
+abbrev LeanLib.facetBuildKey (self : LeanLib) (facet : Name) : BuildKey :=
+  .targetFacet self.pkg.name self.name (`leanLib ++ facet)
 
 abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
   .targetFacet self.pkg.name self.name exeFacet
@@ -69,9 +61,7 @@ abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
 abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
 | moduleFacet m f => m.facetBuildKey f
 | packageFacet p f => p.facetBuildKey f
-| leanLib l => l.leanBuildKey
-| staticLeanLib l => l.staticBuildKey
-| sharedLeanLib l => l.sharedBuildKey
+| libraryFacet l f => l.facetBuildKey f
 | leanExe x => x.buildKey
 | staticExternLib l => l.staticBuildKey
 | sharedExternLib l => l.sharedBuildKey
@@ -91,16 +81,8 @@ instance [FamilyDef CustomData (p.name, t) α]
 : FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [FamilyDef TargetData LeanLib.leanFacet α]
-: FamilyDef BuildData (BuildInfo.key (.leanLib l)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
-instance [FamilyDef TargetData LeanLib.staticFacet α]
-: FamilyDef BuildData (BuildInfo.key (.staticLeanLib l)) α where
-  family_key_eq_type := by unfold BuildData; simp
-
-instance [FamilyDef TargetData LeanLib.sharedFacet α]
-: FamilyDef BuildData (BuildInfo.key (.sharedLeanLib l)) α where
+instance [FamilyDef TargetData (`leanLib ++ f) α]
+: FamilyDef BuildData (BuildInfo.key (.libraryFacet l f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
 instance [FamilyDef TargetData LeanExe.exeFacet α]
@@ -194,17 +176,21 @@ abbrev Package.extraDep (self : Package) : BuildInfo :=
 abbrev Package.customTarget (target : Name) (self : Package) : BuildInfo :=
   .customTarget self target
 
+/-- Build info of the Lean library's Lean binaries. -/
+abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo :=
+  .libraryFacet self facet
+
 /-- Build info of the Lean library's Lean binaries. -/
 abbrev LeanLib.lean (self : LeanLib) : BuildInfo :=
-  .leanLib self
+  self.facet leanFacet
 
 /-- Build info of the Lean library's static binary. -/
 abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
-  .staticLeanLib self
+  self.facet staticFacet
 
 /-- Build info of the Lean library's shared binary. -/
 abbrev LeanLib.shared (self : LeanLib) : BuildInfo :=
-  .sharedLeanLib self
+  self.facet sharedFacet
 
 /-- Build info of the Lean executable. -/
 abbrev LeanExe.exe (self : LeanExe) : BuildInfo :=

Diff for: Lake/Build/Roots.lean renamed to Lake/Build/Library.lean

@@ -3,13 +3,11 @@ 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.Info
-import Lake.Build.Store
-import Lake.Build.Targets
+import Lake.Build.Index
 
 namespace Lake
 
-/-! # Build Static Lib -/
+/-! # Build Lean & Static Lib -/
 
 /-- Build and collect the specified facet of the library's local modules. -/
 def LeanLib.recBuildLocalModules
@@ -33,11 +31,19 @@ protected def LeanLib.recBuildLean
   ActiveTarget.collectOpaqueArray (i := PUnit) <|
     ← self.recBuildLocalModules #[Module.leanBinFacet]
 
+/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
+def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
+  mkFacetTargetConfig (·.recBuildLean)
+
 protected def LeanLib.recBuildStatic
 (self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do
   let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active
   staticLibTarget self.staticLibFile oTargets |>.activate
 
+/-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
+def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
+  mkFacetTargetConfig (·.recBuildStatic)
+
 /-! # Build Shared Lib -/
 
 /--
@@ -76,18 +82,17 @@ protected def LeanLib.recBuildShared
   let linkTargets := (← self.recBuildLinks).map Target.active
   leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate
 
-/-! # Build Executable -/
+/-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
+def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
+  mkFacetTargetConfig (·.recBuildShared)
 
-protected def LeanExe.recBuildExe
-(self : LeanExe) : IndexT RecBuildM ActiveFileTarget := do
-  let (_, imports) ← self.root.imports.recBuild
-  let linkTargets := #[Target.active <| ← self.root.o.recBuild]
-  let mut linkTargets ← imports.foldlM (init := linkTargets) fun arr mod => do
-    let mut arr := arr
-    for facet in mod.nativeFacets do
-      arr := arr.push <| Target.active <| ← recBuild <| mod.facet facet.name
-    return arr
-  let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg
-  for dep in deps do for lib in dep.externLibs do
-    linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
-  leanExeTarget self.file linkTargets self.linkArgs |>.activate
+open LeanLib in
+/--
+A library facet name to build function map that contains builders for
+the initial set of Lake package facets (e.g., `lean`, `static`, and `shared`).
+-/
+def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
+  DNameMap.empty
+  |>.insert leanFacet leanFacetConfig
+  |>.insert staticFacet staticFacetConfig
+  |>.insert sharedFacet sharedFacetConfig

Diff for: Lake/CLI/Build.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build
+import Lake.Build.Index
 import Lake.CLI.Error
 
 namespace Lake
@@ -56,13 +56,11 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except
   else
     throw <| CliError.unknownFacet "module" facet
 
-def resolveLibTarget (lib : LeanLib) (facet : Name) : Except CliError BuildSpec :=
-  if facet.isAnonymous || facet = `lean then
+def resolveLibTarget (ws : Workspace) (lib : LeanLib) (facet : Name) : Except CliError BuildSpec :=
+  if facet.isAnonymous then
     return mkBuildSpec lib.lean
-  else if facet = `static then
-    return mkBuildSpec lib.static
-  else if facet = `shared then
-    return mkBuildSpec lib.shared
+  else if let some config := ws.findLibraryFacetConfig? facet then do
+    mkConfigBuildSpec "library" (lib.facet facet) config rfl
   else
     throw <| CliError.unknownFacet "library" facet
 
@@ -100,7 +98,7 @@ def resolveTargetInPackage (ws : Workspace)
   else if let some lib := pkg.findExternLib? target then
     resolveExternLibTarget lib facet
   else if let some lib := pkg.findLeanLib? target then
-    resolveLibTarget lib facet
+    resolveLibTarget ws lib facet
   else if let some mod := pkg.findModule? target then
     resolveModuleTarget ws mod facet
   else
@@ -126,7 +124,7 @@ def resolveTargetInWorkspace (ws : Workspace)
   else if let some lib := ws.findExternLib? target then
     Array.singleton <$> resolveExternLibTarget lib facet
   else if let some lib := ws.findLeanLib? target then
-    Array.singleton <$> resolveLibTarget lib facet
+    Array.singleton <$> resolveLibTarget ws lib facet
   else if let some pkg := ws.findPackage? target then
     resolvePackageTarget ws pkg facet
   else if let some mod := ws.findModule? target then

Diff for: Lake/CLI/Main.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Load
+import Lake.Build.Imports
 import Lake.Util.Error
 import Lake.Util.MainM
 import Lake.Util.Cli

Diff for: Lake/Config/FacetConfig.lean

@@ -40,3 +40,9 @@ abbrev PackageFacetConfig := FacetConfig PackageData Package
 
 /-- A package facet declaration from a configuration file. -/
 abbrev PackageFacetDecl := NamedConfigDecl PackageFacetConfig
+
+/-- A library facet's declarative configuration. -/
+abbrev LibraryFacetConfig := FacetConfig LibraryData LeanLib
+
+/-- A library facet declaration from a configuration file. -/
+abbrev LibraryFacetDecl := NamedConfigDecl LibraryFacetConfig