refactor: lake: generalize targets

src/lake/Lake/Build/Data.lean

@@ -14,51 +14,70 @@ namespace Lake
 /-! ## Build Data Subtypes                                                    -/
 --------------------------------------------------------------------------------
 
+/--
+The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
+facet to its associated build data. For example, an active build target for the
+`externLib.static` facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `target_data`).
+-/
+opaque TargetData (facet : Name) : Type
+
+/-- The type of the output of the `facet` of objects of `kind`. -/
+abbrev FacetData (kind facet : Name) := TargetData (kind ++ facet)
+
+instance [h : FamilyOut (FacetData kind) facet α] : FamilyDef TargetData (kind ++ facet) α :=
+  ⟨h.fam_eq⟩
+
+instance [h : FamilyDef TargetData (kind ++ facet) α] : FamilyDef (FacetData kind) facet α :=
+  ⟨h.fam_eq⟩
+
 /--
 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`.
+in the Lake build store. For example, the generated C file for `c`.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `module_data`).
 -/
-opaque ModuleData (facet : Name) : Type
+abbrev ModuleData := FacetData `module
 
 /--
 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`.
+in the Lake build store. For example, the direct dependencies of the package
+for the `deps` facet.
 
 It is an open type, meaning additional mappings can be add lazily
 as needed (via `package_data`).
 -/
-opaque PackageData (facet : Name) : Type
+abbrev PackageData := FacetData `package
 
 /--
-The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
-facet to its associated build data. For example, an active build target for
-the `externLib.static` facet.
+The open type family which maps a Lean library facet's name to its build data
+in the Lake build store. For example, the generated static library for the
+`static` facet.
 
 It is an open type, meaning additional mappings can be add lazily
-as needed (via `target_data`).
+as needed (via `library_data`).
 -/
-opaque TargetData (facet : Name) : Type
+abbrev LibraryData := FacetData `leanLib
 
-/-
-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.
+@[inherit_doc LibraryData]
+abbrev LeanLibData := LibraryData
 
-It is an open type, meaning additional mappings can be add lazily
-as needed (via `library_data`).
+/--
+The type family which maps a Lean executable facet's name to its build data
+in the Lake build store. For example, the generated executable for the
+`exe` facet.
 -/
-abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet)
-
-instance [h : FamilyOut LibraryData facet α] : FamilyDef TargetData (`leanLib ++ facet) α :=
-  ⟨by simp [h.family_key_eq_type]⟩
+abbrev LeanExeData := FacetData `leanExe
 
-instance [h : FamilyOut TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
-  ⟨h.family_key_eq_type⟩
+/--
+The type family which maps an external library facet's name to its build data
+in the Lake build store. For example, the generated static library for the
+`static` facet.
+-/
+abbrev ExternLibData := FacetData `externLib
 
 /--
 The open type family which maps a custom target (package × target name) to
@@ -79,53 +98,60 @@ It is a simple type function composed of the separate open type families for
 modules facets, package facets, Lake target facets, and custom targets.
 -/
 abbrev BuildData : BuildKey → Type
-| .moduleFacet _ f => ModuleData f
-| .packageFacet _ f => PackageData f
-| .targetFacet _ _ f => TargetData f
-| .customTarget p t => CustomData (p, t)
+| .module _ => TargetData `module
+| .package _ => TargetData `package
+| .packageTarget p t => CustomData (p, t)
+| .facet _ k f => FacetData k f
 
-instance (priority := low) : FamilyDef BuildData k (BuildData k) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
-instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.facet t k f) (FacetData k f) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
 
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/
 --------------------------------------------------------------------------------
 
+open Parser Command
+
+/-- Macro for declaring new `FacetData`. -/
+scoped macro (name := facetDataDecl)
+  doc?:optional(docComment) "facet_data " kind:ident facet:ident " : " ty:term
+: command => do
+  let dty := mkCIdentFrom (← getRef) ``TargetData
+  let kindName := Name.quoteFrom kind kind.getId
+  let facetName := Name.quoteFrom facet facet.getId
+  let id := mkIdentFrom facet (canonical := true) <|
+    facet.getId.modifyBase (kind.getId ++ ·)
+  `($[$doc?]? family_def $id : $dty ($kindName ++ $facetName) := $ty)
+
 /-- Macro for declaring new `PackageData`. -/
-scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
-"package_data " id:ident " : " ty:term : command => do
-  let dty := mkCIdentFrom (← getRef) ``PackageData
-  let key := Name.quoteFrom id id.getId
-  `($[$doc?]? family_def $id : $dty $key := $ty)
+scoped macro (name := packageDataDecl)
+  doc?:optional(docComment) "package_data " facet:ident " : " ty:term
+: command => `($[$doc?]? facet_data $(mkIdent `package) $facet : $ty)
 
 /-- Macro for declaring new `ModuleData`. -/
-scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
-"module_data " id:ident " : " ty:term : command => do
-  let dty := mkCIdentFrom (← getRef) ``ModuleData
-  let key := Name.quoteFrom id id.getId
-  `($[$doc?]? family_def $id : $dty $key := $ty)
+scoped macro (name := moduleDataDecl)
+  doc?:optional(docComment) "module_data " facet:ident " : " ty:term
+: command => `($[$doc?]? facet_data $(mkIdent `module) $facet : $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 (canonical := true) <| id.getId.modifyBase (`leanLib ++ ·)
-  `($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty)
+/-- Macro for declaring new `LibraryData`. -/
+scoped macro (name := libraryDataDecl)
+  doc?:optional(docComment) "library_data " facet:ident " : " ty:term
+: command => `($[$doc?]? facet_data $(mkIdent `leanLib) $facet : $ty)
 
 /-- Macro for declaring new `TargetData`. -/
-scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
-"target_data " id:ident " : " ty:term : command => do
+scoped macro (name := targetDataDecl)
+  doc?:optional(docComment) "target_data " id:ident " : " ty:term
+: command => do
   let dty := mkCIdentFrom (← getRef) ``TargetData
   let key := Name.quoteFrom id id.getId
   `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `CustomData`. -/
-scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
-"custom_data " pkg:ident tgt:ident " : " ty:term : command => do
+scoped macro (name := customDataDecl)
+  doc?:optional(docComment) "custom_data " pkg:ident tgt:ident " : " ty:term
+: command => do
   let dty := mkCIdentFrom (← getRef) ``CustomData
   let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
   let pkg := Name.quoteFrom pkg pkg.getId

src/lake/Lake/Build/Executable.lean

@@ -31,3 +31,15 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
   for dep in deps do for lib in dep.externLibs do
     linkJobs := linkJobs.push <| ← lib.static.fetch
   buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean
+
+/-- The facet configuration for the builtin `LeanExe.exeFacet`. -/
+def LeanExe.exeFacetConfig : LeanExeFacetConfig exeFacet :=
+  mkFacetJobConfig recBuildExe
+
+/--
+A name-configuration map for the initial set of
+Lean executable facets (e.g., `exe`).
+-/
+def LeanExe.initFacetConfigs : DNameMap LeanExeFacetConfig :=
+  DNameMap.empty
+  |>.insert exeFacet exeFacetConfig

src/lake/Lake/Build/ExternLib.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lake.Build.Common
+
+/-! # External Library Build
+Build function definitions for external libraries.
+-/
+
+open System (FilePath)
+
+namespace Lake
+
+def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
+  withRegisterJob s!"{lib.staticTargetName.toString}:static" do
+  lib.config.getPath <$> fetch (lib.pkg.target lib.staticTargetName)
+
+/-- The facet configuration for the builtin `ExternLib.staticFacet`. -/
+def ExternLib.staticFacetConfig : ExternLibFacetConfig staticFacet :=
+  mkFacetJobConfig recBuildStatic
+
+def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
+  withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
+  buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
+
+/-- The facet configuration for the builtin `ExternLib.sharedFacet`. -/
+def ExternLib.sharedFacetConfig : ExternLibFacetConfig sharedFacet :=
+  mkFacetJobConfig recBuildShared
+
+def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
+  withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
+  computeDynlibOfShared (← lib.shared.fetch)
+
+/-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
+def ExternLib.dynlibFacetConfig : ExternLibFacetConfig dynlibFacet :=
+  mkFacetJobConfig recComputeDynlib
+
+/--
+A name-configuration map for the initial set of
+external library facets (e.g., `static`, `shared`).
+-/
+def ExternLib.initFacetConfigs : DNameMap ExternLibFacetConfig :=
+  DNameMap.empty
+  |>.insert staticFacet staticFacetConfig
+  |>.insert sharedFacet sharedFacetConfig
+  |>.insert dynlibFacet dynlibFacetConfig

src/lake/Lake/Build/Facets.lean

@@ -41,7 +41,7 @@ instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
   ⟨facet.data_eq⟩
 
 instance [FamilyOut ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
-  ⟨facet, FamilyOut.family_key_eq_type⟩
+  ⟨facet, FamilyOut.fam_eq⟩
 
 /--
 The facet which builds all of a module's dependencies
@@ -189,17 +189,17 @@ abbrev LeanLib.extraDepFacet := `extraDep
 library_data extraDep : Unit
 
 /-- A Lean binary executable. -/
-abbrev LeanExe.exeFacet := `leanExe
-target_data leanExe : FilePath
+abbrev LeanExe.exeFacet := `exe
+facet_data leanExe exe : FilePath
 
 /-- A external library's static binary. -/
-abbrev ExternLib.staticFacet := `externLib.static
-target_data externLib.static : FilePath
+abbrev ExternLib.staticFacet := `static
+facet_data externLib static : FilePath
 
 /-- A external library's shared binary. -/
-abbrev ExternLib.sharedFacet := `externLib.shared
-target_data externLib.shared : FilePath
+abbrev ExternLib.sharedFacet := `shared
+facet_data externLib shared : FilePath
 
 /-- A external library's dynlib. -/
-abbrev ExternLib.dynlibFacet := `externLib.dynlib
-target_data externLib.dynlib : Dynlib
+abbrev ExternLib.dynlibFacet := `dynlib
+facet_data externLib dynlib : Dynlib

src/lake/Lake/Build/Index.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Build.Executable
+import Lake.Build.ExternLib
 import Lake.Build.Topological
 
 /-!
@@ -16,31 +17,27 @@ Lake build functions, which is used by Lake to build any Lake build info.
 This module leverages the index to perform topologically-based recursive builds.
 -/
 
-open Lean
-namespace Lake
+open Lean (Name)
 open System (FilePath)
 
+namespace Lake
+
 /--
 Converts a conveniently-typed target facet build function into its
 dynamically-typed equivalent.
 -/
-@[macro_inline] def mkTargetFacetBuild
+@[macro_inline, deprecated "Deprecated without replacement." (since := "2025-02-27")]
+def mkTargetFacetBuild
   (facet : Name) (build : FetchM (Job α))
   [h : FamilyOut TargetData facet α]
 : FetchM (Job (TargetData facet)) :=
-  cast (by rw [← h.family_key_eq_type]) build
+  cast (by rw [← h.fam_eq]) build
 
-def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
-  withRegisterJob s!"{lib.staticTargetName.toString}:static" do
-  lib.config.getPath <$> fetch (lib.pkg.target lib.staticTargetName)
-
-def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
-  withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
-  buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
-
-def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
-  withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
-  computeDynlibOfShared (← lib.shared.fetch)
+@[inline] private def FacetConfig.recBuild
+  [h : FamilyOut TargetData kind α]
+  (self : FacetConfig kind facet) (info : α)
+: FetchM (Job (FacetData kind facet)) :=
+  self.fetchFn <| cast (by simp) info
 
 /-!
 ## Topologically-based Recursive Build Using the Index
@@ -50,12 +47,12 @@ def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
 def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
 | .moduleFacet mod facet => do
   if let some config := (← getWorkspace).findModuleFacetConfig? facet then
-    config.fetchFn mod
+    config.recBuild mod
   else
     error s!"do not know how to fetch module facet `{facet}`"
 | .packageFacet pkg facet => do
   if let some config := (← getWorkspace).findPackageFacetConfig? facet then
-    config.fetchFn pkg
+    config.recBuild pkg
   else
     error s!"do not know how to fetch package facet `{facet}`"
 | .target pkg target =>
@@ -65,17 +62,17 @@ def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
     error s!"could not fetch `{target}` of `{pkg.name}` -- target not found"
 | .libraryFacet lib facet => do
   if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
-    config.fetchFn lib
+    config.recBuild lib
   else
     error s!"do not know how to fetch library facet `{facet}`"
 | .leanExe exe =>
-  mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
+  LeanExe.exeFacetConfig.recBuild exe
 | .staticExternLib lib =>
-  mkTargetFacetBuild ExternLib.staticFacet lib.recBuildStatic
+  ExternLib.staticFacetConfig.recBuild lib
 | .sharedExternLib lib =>
-  mkTargetFacetBuild ExternLib.sharedFacet lib.recBuildShared
+  ExternLib.sharedFacetConfig.recBuild lib
 | .dynlibExternLib lib =>
-  mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
+  ExternLib.dynlibFacetConfig.recBuild lib
 
 /-- Recursive build function with memoization. -/
 def recFetchWithIndex : (info : BuildInfo) → RecBuildM (Job (BuildData info.key)) :=