feat: recursive builds in extern_lib

Lake/Build/Index.lean

@@ -26,6 +26,12 @@ dynamically typed equivalent.
 [h : FamilyDef TargetData facet α] : IndexBuildM (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
+def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+  if let some target := lib.pkg.findTargetConfig? (.str lib.name "static") then
+    lib.config.getJob <$> (target.build lib.pkg)
+  else
+    error "missing target for external library"
+
 def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
   buildLeanSharedLibOfStatic (← lib.static.recBuild) lib.linkArgs
 
@@ -61,7 +67,7 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
 | .leanExe exe =>
   mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
 | .staticExternLib lib =>
-  mkTargetFacetBuild ExternLib.staticFacet lib.build
+  mkTargetFacetBuild ExternLib.staticFacet lib.recBuildStatic
 | .sharedExternLib lib =>
   mkTargetFacetBuild ExternLib.sharedFacet lib.recBuildShared
 | .dynlibExternLib lib =>

Lake/Build/Info.lean

@@ -7,6 +7,7 @@ import Lake.Config.LeanExe
 import Lake.Config.ExternLib
 import Lake.Build.Facets
 import Lake.Util.EquipT
+import Lake.Util.Fact
 
 /-!
 # Build Info
@@ -82,6 +83,10 @@ instance [FamilyDef PackageData f α]
 : FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
+instance [h : Fact (p.name = n)] [FamilyDef CustomData (n, t) α]
+: FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
+  family_key_eq_type := by unfold BuildData; simp [h.proof]
+
 instance [FamilyDef CustomData (p.name, t) α]
 : FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
   family_key_eq_type := by unfold BuildData; simp

Lake/Config/ExternLib.lean

@@ -11,28 +11,22 @@ namespace Lake
 structure ExternLib where
   /-- The package the library belongs to. -/
   pkg : Package
-   /-- The library's user-defined configuration. -/
-  config : ExternLibConfig
+  /-- The external library's name. -/
+  name : Name
+  /-- The library's user-defined configuration. -/
+  config : ExternLibConfig pkg.name name
   deriving Inhabited
 
 /-- The external libraries of the package (as an Array). -/
 @[inline] def Package.externLibs (self : Package) : Array ExternLib :=
-  self.externLibConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[]
+  self.externLibConfigs.fold (fun a n v => a.push (⟨self, n, v⟩)) #[]
 
 /-- Try to find a external library in the package with the given name. -/
 @[inline] def Package.findExternLib? (name : Name) (self : Package) : Option ExternLib :=
-  self.externLibConfigs.find? name |>.map (⟨self, ·⟩)
+  self.externLibConfigs.find? name |>.map (⟨self, name, ·⟩)
 
 namespace ExternLib
 
-/-- The library's well-formed name. -/
-@[inline] def name (self : ExternLib) : Name :=
-  self.config.name
-
-/-- The external library's user-defined `build`. -/
-@[inline] def build (self : ExternLib) : SchedulerM (BuildJob FilePath) :=
-  self.config.build
-
 /--
 The arguments to pass to `leanc` when linking the external library.
 That is, the package's `moreLinkArgs`.

Lake/Config/ExternLibConfig.lean

@@ -9,9 +9,13 @@ namespace Lake
 open Lean System
 
 /-- A external library's declarative configuration. -/
-structure ExternLibConfig where
-  /-- The name of the target. -/
-  name : Name
-  /-- The library's build. -/
-  build : SchedulerM (BuildJob FilePath)
+structure ExternLibConfig (pkgName name : Name) where
+  /-- The library's build data. -/
+  getJob : CustomData (pkgName, .str name "static") → BuildJob FilePath
   deriving Inhabited
+
+/-- A dependently typed configuration based on its registered package and name. -/
+structure ExternLibDecl where
+  pkg : Name
+  name : Name
+  config : ExternLibConfig pkg name

Lake/Config/Package.lean

@@ -193,7 +193,7 @@ structure Package where
   /-- Lean binary executable configurations for the package. -/
   leanExeConfigs : NameMap LeanExeConfig := {}
   /-- External library targets for the package. -/
-  externLibConfigs : NameMap ExternLibConfig := {}
+  externLibConfigs : DNameMap (ExternLibConfig config.name) := {}
   /-- (Opaque references to) targets defined in the package. -/
   opaqueTargetConfigs : DNameMap (OpaqueTargetConfig config.name) := {}
   /--

Lake/Config/TargetConfig.lean

@@ -11,13 +11,15 @@ namespace Lake
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
-  build : Package → IndexBuildM (CustomData (pkgName, name))
+  build : (pkg : Package) → [Fact (pkg.name = pkgName)] →
+    IndexBuildM (CustomData (pkgName, name))
   /-- Does this target produce an associated asynchronous job? -/
   getJob? : Option (CustomData (pkgName, name) → Job Unit)
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
-@[inline] def mkTargetJobConfig (build : Package → IndexBuildM (BuildJob α))
+@[inline] def mkTargetJobConfig
+(build : (pkg : Package) → [Fact (pkg.name = pkgName)] → IndexBuildM (BuildJob α))
 [h : FamilyDef CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob? := some fun data => discard <| ofFamily data

Lake/DSL/Facets.lean

@@ -27,7 +27,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do
       $[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig $defn
-      })
+      } $[$wds?]?)
   | stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
 
 scoped macro (name := packageFacetDecl)
@@ -42,7 +42,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do
       $[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig $defn
-      })
+      } $[$wds?]?)
   | stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
 
 scoped macro (name := libraryFacetDecl)
@@ -57,7 +57,7 @@ kw:"library_facet " sig:simpleDeclSig : command => do
       $[$doc?]? @[$attrs,*] def $id : LibraryFacetDecl := {
         name := $name
         config := Lake.mkFacetJobConfig $defn
-      })
+      } $[$wds?]?)
   | stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
 
 scoped macro (name := targetDecl)
@@ -74,5 +74,40 @@ kw:"target " sig:simpleDeclSig : command => do
         pkg := $pkgName
         name := $name
         config := Lake.mkTargetJobConfig $defn
-      })
+      }  $[$wds?]?)
   | stx => Macro.throwErrorAt stx "ill-formed target declaration"
+
+--------------------------------------------------------------------------------
+/-! # External Library Target -/
+--------------------------------------------------------------------------------
+
+syntax externLibDeclSpec :=
+  ident declValSimple
+
+/--
+Define a new external library target for the package. Has one form:
+
+```lean
+extern_lib «target-name» := /- build function term -/
+```
+
+The term should be of type `Package → IndexBuildM (BuildJob FilePath)` and
+build the external library's **static** library.
+-/
+scoped macro (name := externLibDecl)
+doc?:optional(docComment) attrs?:optional(Term.attributes)
+"extern_lib " spec:externLibDeclSpec : command => do
+  match spec with
+  | `(externLibDeclSpec| $id:ident := $defn $[$wds?]?) =>
+    let attr ← `(Term.attrInstance| externLib)
+    let attrs := #[attr] ++ expandAttrs attrs?
+    let pkgName := mkIdentFrom id `_package.name
+    let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
+    let name := Name.quoteFrom id id.getId
+    `(target $targetId : FilePath := $defn $[$wds?]?
+      $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := {
+        pkg := $pkgName
+        name := $name
+        config := {getJob := ofFamily}
+      })
+  | stx => Macro.throwErrorAt stx "ill-formed external library declaration"

Lake/DSL/Targets.lean

@@ -55,29 +55,3 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
   let ty := mkCIdentFrom (← getRef) ``LeanExeConfig
   let attrs := #[attr] ++ expandAttrs attrs?
   mkConfigStructDecl none doc? attrs ty sig
-
---------------------------------------------------------------------------------
-/-! # External Library Target -/
---------------------------------------------------------------------------------
-
-syntax externLibDeclSpec :=
-  ident optional(Term.typeSpec) declValSimple
-
-/--
-Define a new external library target for the package. Has one form:
-
-```lean
-extern_lib «target-name» := /- term of type `FileTarget` -/
-```
--/
-scoped macro (name := externLibDecl)
-doc?:optional(docComment) attrs?:optional(Term.attributes)
-"extern_lib " spec:externLibDeclSpec : command => do
-  match spec with
-  | `(externLibDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
-    let attr ← `(Term.attrInstance| externLib)
-    let ty := ty?.getD <| mkCIdentFrom (← getRef) ``ExternLibConfig
-    let attrs := #[attr] ++ expandAttrs attrs?
-    `($[$doc?]? @[$attrs,*] def $id : $ty :=
-      {name := $(quote id.getId), build := $defn} $[$wds?]?)
-  | stx => Macro.throwErrorAt stx "ill-formed external library declaration"

Lake/Load/Package.lean

@@ -73,8 +73,14 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
     evalConstCheck env opts LeanLibConfig ``LeanLibConfig name
   let leanExeConfigs ← IO.ofExcept <| mkTagMap env leanExeAttr fun name =>
     evalConstCheck env opts LeanExeConfig ``LeanExeConfig name
-  let externLibConfigs ← IO.ofExcept <| mkTagMap env externLibAttr fun name =>
-    evalConstCheck env opts ExternLibConfig ``ExternLibConfig name
+  let externLibConfigs ← mkDTagMap env externLibAttr fun name =>
+    match evalConstCheck env opts ExternLibDecl ``ExternLibDecl name with
+    | .ok decl =>
+      if h : decl.pkg = self.config.name ∧ decl.name = name then
+        return h.1 ▸ h.2 ▸ decl.config
+      else
+        error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`"
+    | .error e => error e
   let opaqueTargetConfigs ← mkDTagMap env targetAttr fun name =>
     match evalConstCheck env opts TargetDecl ``TargetDecl name with
     | .ok decl =>

Lake/Util/Fact.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+/-- Type class synthesis of propositions. -/
+class Fact (P : Prop) : Prop where
+  proof : P
+
+instance : Fact (a = a) := ⟨rfl⟩

examples/ffi/lib/lakefile.lean

@@ -12,17 +12,14 @@ lean_lib FFI
   root := `Main
 }
 
-def pkgDir := __dir__
-def cSrcDir := pkgDir / "c"
-def cBuildDir := pkgDir / _package.buildDir / "c"
-
-def buildFfiO : SchedulerM (BuildJob FilePath) := do
-  let oFile := cBuildDir / "ffi.o"
-  let srcJob ← inputFile <| cSrcDir / "ffi.cpp"
+target ffi.o : FilePath := fun pkg _ => do
+  let oFile := pkg.buildDir / "c" / "ffi.o"
+  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
   buildFileAfterDep oFile srcJob fun srcFile => do
     let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
     compileO "ffi.c" oFile srcFile flags "c++"
 
-extern_lib libleanffi := do
+extern_lib libleanffi := fun pkg _ => do
   let name := nameToStaticLib "leanffi"
-  buildStaticLib (cBuildDir / name) #[← buildFfiO]
+  let ffiO ← recBuild <| pkg.customTarget ``ffi.o
+  buildStaticLib (pkg.buildDir / "c" / name) #[ffiO]

examples/targets/lakefile.lean

@@ -17,14 +17,14 @@ lean_exe b
 lean_exe c
 
 @[defaultTarget]
-target meow : Unit := fun pkg => do
+target meow : Unit := fun pkg _ => do
   IO.FS.writeFile (pkg.buildDir / "meow.txt") "Meow!"
   return .nil
 
-target bark : Unit := fun _pkg => do
+target bark : Unit := fun _pkg _ => do
   logInfo "Bark!"
   return .nil
 
-package_facet print_name : Unit := fun pkg => do
+package_facet print_name : Unit := fun pkg _ => do
   IO.println pkg.name
   return .nil