refactor: move lib/exe targets into the index

Author: tydeu

Diff for: Lake/Build.lean

@@ -5,6 +5,5 @@ Authors: Mac Malone
 -/
 import Lake.Build.Monad
 import Lake.Build.Actions
-import Lake.Build.LeanLib
-import Lake.Build.LeanExe
+import Lake.Build.LeanTarget
 import Lake.Build.Imports

Diff for: Lake/Build/Data.lean

@@ -23,21 +23,20 @@ opaque ModuleData (facet : WfName) : Type
 opaque PackageData (facet : WfName) : Type
 
 /-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
-opaque TargetData (key : BuildKey) : Type
-
+opaque TargetData (facet : WfName) : Type
 
 /--
 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,
 packages, and targets.
 -/
-def BuildData (key : BuildKey) :=
+abbrev BuildData (key : BuildKey) :=
   if key.isModuleKey then
     ModuleData key.facet
   else if key.isPackageKey then
     PackageData key.facet
   else
-    TargetData key
+    TargetData key.facet
 
 theorem isModuleKey_data {k : BuildKey}
 (h : k.isModuleKey = true) : BuildData k = ModuleData k.facet := by
@@ -52,15 +51,20 @@ instance (k : ModuleBuildKey f)
 theorem isPackageKey_data {k : BuildKey}
 (h : k.isPackageKey = true) : BuildData k = PackageData k.facet := by
   unfold BuildData, BuildKey.isModuleKey
-  have has_pkg := of_decide_eq_true (of_decide_eq_true h |>.1)
-  simp [has_pkg, h]
+  simp [of_decide_eq_true (of_decide_eq_true h |>.1), h]
 
 instance (k : PackageBuildKey f)
 [t : DynamicType PackageData f α] : DynamicType BuildData k α where
   eq_dynamic_type := by
     have h := isPackageKey_data k.is_package_key
     simp [h, k.facet_eq_fixed, t.eq_dynamic_type]
 
+theorem isTargetKey_data {k : BuildKey}
+(h : k.isTargetKey = true) : BuildData k = TargetData k.facet := by
+  unfold BuildData, BuildKey.isModuleKey, BuildKey.isPackageKey
+  have ⟨has_p, has_t⟩ := of_decide_eq_true h
+  simp [of_decide_eq_true has_p, of_decide_eq_true has_t, h]
+
 /-- Macro for declaring new `PackageData`. -/
 scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
 "package_data " id:ident " : " ty:term : command => do
@@ -74,3 +78,10 @@ scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
   let dty := mkCIdentFrom (← getRef) ``ModuleData
   let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
   `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+
+/-- Macro for declaring new `TargetData`. -/
+scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
+"target_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``TargetData
+  let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
+  `($[$doc?]? dynamic_data $id : $dty $key := $ty)

Diff for: Lake/Build/Imports.lean

@@ -36,7 +36,7 @@ as "Lean-only". Otherwise, also build `.c` files.
 def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
-    buildPackageFacet self &`extraDep >>= (·.buildOpaque)
+    self.buildFacet &`extraDep >>= (·.buildOpaque)
     return #[]
   else
     -- build local imports from list
@@ -50,9 +50,9 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
         buildModuleTop mod &`lean.c <&> (·.withoutInfo)
     let importTargets ← failOnBuildCycle res
     let dynlibTargets := bStore.collectModuleFacetArray &`lean.dynlib
-    let externLibTargets := bStore.collectPackageFacetArray &`externSharedLibs
+    let externLibTargets := bStore.collectSharedExternLibs
     importTargets.forM (·.buildOpaque)
     let dynlibs ← dynlibTargets.mapM (·.build)
-    let externLibs ← externLibTargets.concatMapM (·.mapM (·.build))
+    let externLibs ← externLibTargets.mapM (·.build)
     -- Note: Lean wants the external library symbols before module symbols
     return  externLibs ++ dynlibs

Diff for: Lake/Build/Index.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Module1
+import Lake.Build.LeanTarget1
 import Lake.Build.Topological
 import Lake.Util.EStateT
 
@@ -38,6 +39,13 @@ abbrev PackageBuildMap (m : Type → Type v) :=
 
 @[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
 
+/-- A map from target facet names to build functions. -/
+abbrev TargetBuildMap (m : Type → Type v) :=
+  DRBMap WfName (cmp := WfName.quickCmp) fun k =>
+    Package → IndexBuildFn m → m (PackageData k)
+
+@[inline] def TargetBuildMap.empty : PackageBuildMap m := DRBMap.empty
+
 /-!
 ## Build Function Constructor Helpers
 -/
@@ -58,6 +66,14 @@ dynamically typed equivalent.
 [h : DynamicType PackageData facet α] : Package → IndexT m (PackageData facet) :=
   cast (by rw [← h.eq_dynamic_type]) build
 
+/--
+Converts a conveniently typed target build function into its
+dynamically typed equivalent.
+-/
+@[inline] def mkTargetBuild (facet : WfName) (build : IndexT m α)
+[h : DynamicType TargetData facet α] : IndexT m (TargetData facet) :=
+  cast (by rw [← h.eq_dynamic_type]) build
+
 section
 variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
 
@@ -127,15 +143,6 @@ the initial set of Lake package facets (e.g., `extraDep`).
         target ← target.mixOpaqueAsync extraDepTarget
     target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
   )
-  -- Build the `extern_lib` targets of the package
-  |>.insert &`externSharedLibs (mkPackageFacetBuild <| fun pkg => do
-    let mut targets := #[]
-    for (_, config) in pkg.externLibConfigs.toList do
-      let target := staticToLeanDynlibTarget config.target
-      targets := targets.push <| ← target.activate
-    return targets
-  )
-
 /-!
 ## Topologically-based Recursive Build Using the Index
 -/
@@ -154,6 +161,16 @@ the initial set of Lake package facets (e.g., `extraDep`).
       build pkg
     else
       error s!"do not know how to build package facet `{facet}`"
+  | .staticLeanLib lib =>
+    mkTargetBuild &`leanLib.static lib.recBuildStatic
+  | .sharedLeanLib lib =>
+    mkTargetBuild &`leanLib.shared lib.recBuildShared
+  | .leanExe exe =>
+    mkTargetBuild &`leanExe exe.recBuild
+  | .staticExternLib lib =>
+    mkTargetBuild &`externLib.static <| lib.target.activate
+  | .sharedExternLib lib =>
+    mkTargetBuild &`externLib.shared <| staticToLeanDynlibTarget (lib.target) |>.activate
   | _ =>
     error s!"do not know how to build `{info.key}`"
 
@@ -171,7 +188,9 @@ of the top-level build.
 -/
 @[inline] def buildPackageTop (pkg : Package) (facet : WfName)
 [h : DynamicType PackageData facet α] : CycleT BuildKey m α  :=
-  have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
+  have of_data := by
+    unfold BuildData, BuildInfo.key, Package.mkBuildKey
+    simp [h.eq_dynamic_type]
   cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
 
 end
@@ -184,8 +203,7 @@ end
 Recursively build the specified facet of the given package,
 returning the result.
 -/
-def buildPackageFacet
-(pkg : Package) (facet : WfName)
+def Package.buildFacet (self : Package) (facet : WfName)
 [DynamicType PackageData facet α] : BuildM α := do
   failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
-    buildPackageTop pkg facet
+    buildPackageTop self facet

Diff for: Lake/Build/Info.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Data
-import Lake.Config.Module
+import Lake.Config.LeanExe
+import Lake.Config.ExternLib
 import Lake.Util.EquipT
 
 namespace Lake
@@ -17,17 +18,42 @@ namespace Lake
 @[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
   ⟨⟨self.name, none, facet⟩, rfl, rfl⟩
 
+abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`leanLib.static⟩
+
+abbrev LeanLib.sharedBuildKey (self : LeanLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`leanLib.shared⟩
+
+abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`leanExe⟩
+
+abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`externLib.static⟩
+
+abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
+  ⟨self.pkg.name, self.name, &`externLib.shared⟩
+
 -- # 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)
 | target (package : Package) (target : WfName) (facet : WfName)
 
 def BuildInfo.key : (self : BuildInfo) → BuildKey
-| module m f => ⟨none, m.name, f⟩
-| package p f => ⟨p.name, none, f⟩
+| module m f => m.mkBuildKey f
+| package p f => p.mkBuildKey f
+| staticLeanLib l => l.staticBuildKey
+| sharedLeanLib l => l.sharedBuildKey
+| leanExe x => x.buildKey
+| staticExternLib l => l.staticBuildKey
+| sharedExternLib l => l.sharedBuildKey
 | target p t f => ⟨p.name, t, f⟩
 
 /-- A build function for any element of the Lake build index. -/
@@ -38,15 +64,29 @@ abbrev IndexBuildFn (m : Type → Type v) :=
 /-- A transformer to equip a monad with a build function for the Lake index. -/
 abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 
-@[inline] def Module.recBuildFacet (mod : Module) (facet : WfName)
+@[inline] def Module.recBuildFacet (self : Module) (facet : WfName)
 [DynamicType ModuleData facet α] : IndexT m α := fun build =>
-  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.module mod facet
+  let to_data := by
+    unfold BuildData, BuildInfo.key, Module.mkBuildKey
+    simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.module self facet
 
-@[inline] def Package.recBuildFacet (pkg : Package) (facet : WfName)
+@[inline] def Package.recBuildFacet (self : Package) (facet : WfName)
 [DynamicType PackageData facet α] : IndexT m α := fun build =>
+  let to_data := by
+    unfold BuildData, BuildInfo.key, Package.mkBuildKey
+    simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.package self facet
+
+@[inline] def ExternLib.recBuildStatic (self : ExternLib)
+[DynamicType TargetData &`externLib.static α] : IndexT m α := fun build =>
   let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
-  cast to_data <| build <| BuildInfo.package pkg facet
+  cast to_data <| build <| BuildInfo.staticExternLib self
+
+@[inline] def ExternLib.recBuildShared (self : ExternLib)
+[DynamicType TargetData &`externLib.shared α] : IndexT m α := fun build =>
+  let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
+  cast to_data <| build <| BuildInfo.sharedExternLib self
 
 -- # Data Types of Build Results
 
@@ -81,5 +121,19 @@ package_data deps : Array Package
 /-- The package's `extraDepTarget`. -/
 package_data extraDep : ActiveOpaqueTarget
 
-/-- The package's `extern_lib` targets compiled into shared libraries. -/
-package_data externSharedLibs : Array ActiveFileTarget
+-- ## 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 for: Lake/Build/Key.lean

@@ -62,6 +62,9 @@ namespace BuildKey
 @[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by
   simp [BuildKey.isPackageKey]
 
+@[simp] theorem not_isPackageKey_target : ¬BuildKey.isPackageKey ⟨o, some t, f⟩ := by
+  simp [BuildKey.isPackageKey]
+
 @[inline] def isTargetKey (self : BuildKey) : Bool :=
   self.hasPackage ∧ self.hasTarget