From a05e35c783c1b94ff397cc6227fbf6a7c901bdbb Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 26 Jul 2022 15:07:27 -0400
Subject: [PATCH] feat: library facets

---
 Lake/Build.lean                         |  1 +
 Lake/Build/Data.lean                    | 25 +++++++++++++--
 Lake/Build/Executable.lean              | 26 ++++++++++++++++
 Lake/Build/Facets.lean                  | 12 ++++----
 Lake/Build/Index.lean                   | 17 +++++-----
 Lake/Build/Info.lean                    | 40 ++++++++----------------
 Lake/Build/{Roots.lean => Library.lean} | 41 ++++++++++++++-----------
 Lake/CLI/Build.lean                     | 16 +++++-----
 Lake/CLI/Main.lean                      |  1 +
 Lake/Config/FacetConfig.lean            |  6 ++++
 Lake/Config/Workspace.lean              | 24 +++++++++------
 Lake/DSL/Attributes.lean                |  3 ++
 Lake/DSL/Facets.lean                    | 15 +++++++++
 Lake/Load/Main.lean                     |  8 +++--
 Lake/Load/Package.lean                  | 17 ++++++++--
 15 files changed, 165 insertions(+), 87 deletions(-)
 create mode 100644 Lake/Build/Executable.lean
 rename Lake/Build/{Roots.lean => Library.lean} (73%)

diff --git a/Lake/Build.lean b/Lake/Build.lean
index 79da525787..446f79716e 100644
--- a/Lake/Build.lean
+++ b/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 --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
index ccb14ed1a8..909e73048a 100644
--- a/Lake/Build/Data.lean
+++ b/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 --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean
new file mode 100644
index 0000000000..7eef1238cc
--- /dev/null
+++ b/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 --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean
index 09edcf1f91..8516d94351 100644
--- a/Lake/Build/Facets.lean
+++ b/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 --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index e397860bf2..6e23368416 100644
--- a/Lake/Build/Index.lean
+++ b/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 --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index dcd9244757..f9e649472c 100644
--- a/Lake/Build/Info.lean
+++ b/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 --git a/Lake/Build/Roots.lean b/Lake/Build/Library.lean
similarity index 73%
rename from Lake/Build/Roots.lean
rename to Lake/Build/Library.lean
index 0b1e1e79de..0758a63990 100644
--- a/Lake/Build/Roots.lean
+++ b/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 --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index 00a10fb0ba..c6744689ad 100644
--- a/Lake/CLI/Build.lean
+++ b/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 --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index 132a2a9c85..4516b517ce 100644
--- a/Lake/CLI/Main.lean
+++ b/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 --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean
index 568bcaaca8..60efcdd161 100644
--- a/Lake/Config/FacetConfig.lean
+++ b/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
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 4e27edcab4..f775388186 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -24,16 +24,12 @@ structure Workspace : Type where
   lakeEnv : Lake.Env
   /-- Name-package map of packages within the workspace. -/
   packageMap : NameMap Package := {}
-  /--
-  Name-configuration map of (opaque references to)
-  module facets defined in the workspace.
-  -/
-  moduleFacetConfigs : DNameMap ModuleFacetConfig := {}
-  /--
-  Name-configuration map of (opaque references to)
-  module facets defined in the workspace.
-  -/
-  packageFacetConfigs : DNameMap PackageFacetConfig := {}
+  /-- Name-configuration map of module facets defined in the workspace. -/
+  moduleFacetConfigs : DNameMap ModuleFacetConfig
+  /-- Name-configuration map of package facets defined in the workspace. -/
+  packageFacetConfigs : DNameMap PackageFacetConfig
+  /-- Name-configuration map of library facets defined in the workspace. -/
+  libraryFacetConfigs : DNameMap LibraryFacetConfig
   deriving Inhabited
 
 hydrate_opaque_type OpaqueWorkspace Workspace
@@ -116,6 +112,14 @@ def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : W
 def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
   self.packageFacetConfigs.find? name
 
+/-- Add a library facet to the workspace. -/
+def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
+  {self with libraryFacetConfigs := self.libraryFacetConfigs.insert cfg.name cfg}
+
+/-- Try to find a library facet configuration in the workspace with the given name. -/
+def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
+  self.libraryFacetConfigs.find? name
+
 /-- The `LEAN_PATH` of the workspace. -/
 def leanPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.oleanDir)
diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean
index 998028a790..c930bc77ec 100644
--- a/Lake/DSL/Attributes.lean
+++ b/Lake/DSL/Attributes.lean
@@ -45,3 +45,6 @@ initialize moduleFacetAttr : TagAttribute ←
 
 initialize packageFacetAttr : TagAttribute ←
   registerTagAttribute `packageFacet "mark a definition as a Lake package facet"
+
+initialize libraryFacetAttr : TagAttribute ←
+  registerTagAttribute `libraryFacet "mark a definition as a Lake library facet"
diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean
index f77428e921..71b9a9f099 100644
--- a/Lake/DSL/Facets.lean
+++ b/Lake/DSL/Facets.lean
@@ -45,6 +45,21 @@ kw:"package_facet " sig:simpleDeclSig : command => do
       })
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
+scoped macro (name := libraryFacetDecl)
+doc?:optional(docComment) attrs?:optional(Term.attributes)
+kw:"library_facet " sig:simpleDeclSig : command => do
+  match sig with
+  | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) =>
+    let attr ← withRef kw `(Term.attrInstance| libraryFacet)
+    let attrs := #[attr] ++ expandAttrs attrs?
+    let name := Name.quoteFrom id id.getId
+    `(library_data $id : ActiveBuildTarget $ty
+      $[$doc?]? @[$attrs,*] def $id : LibraryFacetDecl := {
+        name := $name
+        config := Lake.mkFacetTargetConfig $defn
+      })
+  | stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
+
 scoped macro (name := targetDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"target " sig:simpleDeclSig : command => do
diff --git a/Lake/Load/Main.lean b/Lake/Load/Main.lean
index 5ca5576743..c389f692e1 100644
--- a/Lake/Load/Main.lean
+++ b/Lake/Load/Main.lean
@@ -9,6 +9,7 @@ import Lake.Config.Workspace
 import Lake.Build.Topological
 import Lake.Build.Module
 import Lake.Build.Package
+import Lake.Build.Library
 import Lake.Load.Materialize
 import Lake.Load.Package
 import Lake.Load.Elab
@@ -19,7 +20,7 @@ namespace Lake
 
 /--
 Elaborate a package configuration file and
-construct a bare `Package` from its `PackageConfig` file.
+construct a bare `Package` from its `PackageConfig` definition.
 -/
 def loadPkg (dir : FilePath) (configOpts : NameMap String)
 (leanOpts := Options.empty) (configFile := dir / defaultConfigFile) : LogIO Package := do
@@ -60,7 +61,7 @@ where
         s!"but resolved dependency has name {depPkg.name} (in {dir})"
     let depDeps ← IO.ofExcept <| loadDeps depPkg.configEnv leanOpts
     let depDepPkgs ← depDeps.mapM fun dep => resolve (depPkg, dep)
-    set (← (← get).loadFacets depPkg.configEnv depPkg.leanOpts)
+    set (← IO.ofExcept <| (← get).addFacetsFromEnv depPkg.configEnv depPkg.leanOpts)
     let depPkg ← depPkg.finalize depDepPkgs
     return depPkg
 
@@ -75,6 +76,7 @@ def loadWorkspace (config : LoadConfig) : LogIO Workspace := do
     root, lakeEnv := config.env
     moduleFacetConfigs := initModuleFacetConfigs
     packageFacetConfigs := initPackageFacetConfigs
+    libraryFacetConfigs := initLibraryFacetConfigs
   }
   let deps ← IO.ofExcept <| loadDeps root.configEnv config.leanOpts
   let manifest ← Manifest.loadFromFile ws.manifestFile |>.catchExceptions fun _ => pure {}
@@ -82,7 +84,7 @@ def loadWorkspace (config : LoadConfig) : LogIO Workspace := do
     config.leanOpts deps config.updateDeps |>.run manifest
   unless manifest.isEmpty do
     manifest.saveToFile ws.manifestFile
-  let ws ← ws.loadFacets root.configEnv root.leanOpts
+  let ws ← IO.ofExcept <| ws.addFacetsFromEnv root.configEnv root.leanOpts
   let root ← root.finalize deps
   let packageMap := ws.packageMap.insert root.name root
   return {ws with root, packageMap}
diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean
index e74d23992a..4631932b0a 100644
--- a/Lake/Load/Package.lean
+++ b/Lake/Load/Package.lean
@@ -6,6 +6,11 @@ Authors: Mac Malone
 import Lake.DSL.Attributes
 import Lake.Config.Workspace
 
+/-!
+This module contains definitions to load configuration objects from
+a package configuration file (e.g., `lakefile.lean`).
+-/
+
 namespace Lake
 open Lean System
 
@@ -91,8 +96,8 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
 /--
 Load module/package facets into a `Workspace` from a configuration environment.
 -/
-def Workspace.loadFacets
-(env : Environment) (opts : Options) (self : Workspace) : LogIO Workspace := do
+def Workspace.addFacetsFromEnv
+(env : Environment) (opts : Options) (self : Workspace) : Except String Workspace := do
   let mut ws := self
   for name in moduleFacetAttr.ext.getState env do
     match evalConstCheck env opts ModuleFacetDecl ``ModuleFacetDecl name with
@@ -110,4 +115,12 @@ def Workspace.loadFacets
       else
         error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
     | .error e => error e
+  for name in libraryFacetAttr.ext.getState env do
+    match evalConstCheck env opts LibraryFacetDecl ``LibraryFacetDecl name with
+    | .ok decl =>
+      if h : name = decl.name then
+        ws := ws.addLibraryFacetConfig <| h ▸ decl.config
+      else
+        error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
+    | .error e => error e
   return ws