feat: multi lib & exe targets w/ updated build CLI syntax

Author: tydeu

Diff for: Lake/Build/Package.lean

@@ -52,9 +52,11 @@ def Package.buildLibModules (self : Package) (lib : LeanLibConfig)
     (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
   buildMods.catchFailure fun _ => pure <| failure
 
-def Package.oleanTarget (self : Package) : OpaqueTarget :=
-  Target.opaque <| self.buildLibModules self.builtinLibConfig
-    recBuildModuleOleanTargetWithLocalImports
+def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
+  Target.opaque <| self.buildLibModules lib recBuildModuleOleanTargetWithLocalImports
+
+def Package.libTarget (self : Package) : OpaqueTarget :=
+  self.mkLibTarget self.builtinLibConfig
 
 -- # Build Specific Modules of the Package
 

Diff for: Lake/CLI/Build.lean

@@ -16,7 +16,8 @@ def Package.defaultTarget (self : Package) : OpaqueTarget :=
   | .bin => self.exeTarget.withoutInfo
   | .staticLib => self.staticLibTarget.withoutInfo
   | .sharedLib => self.sharedLibTarget.withoutInfo
-  | .oleans =>  self.oleanTarget.withoutInfo
+  | .leanLib => self.libTarget.withoutInfo
+  | .oleans => self.libTarget.withoutInfo
 
 def parsePkgSpec (ws : Workspace) (spec : String) : Except CliError Package :=
   if spec.isEmpty then
@@ -26,57 +27,103 @@ def parsePkgSpec (ws : Workspace) (spec : String) : Except CliError Package :=
     | some pkg => return pkg
     | none => throw <| CliError.unknownPackage spec
 
-def parseTargetBaseSpec (ws : Workspace) (spec : String) : Except CliError (Package × Option Name) := do
+def resolveModuleTarget (pkg : Package) (mod : Name) (facet : String) : Except CliError OpaqueTarget :=
+  if pkg.hasModule mod then
+    if facet.isEmpty || facet == "olean" then
+      return pkg.moduleOleanTarget mod |>.withoutInfo
+    else if facet == "c" then
+      return pkg.moduleOleanAndCTarget mod |>.withoutInfo
+    else if facet == "o" then
+      return pkg.moduleOTarget mod |>.withoutInfo
+    else
+      throw <| CliError.unknownFacet "module" facet
+  else
+    throw <| CliError.missingModule pkg.name mod
+
+def resolveLibTarget (pkg : Package) (lib : LeanLibConfig) (facet : String) : Except CliError OpaqueTarget :=
+  if facet.isEmpty || facet == "lean" || facet == "oleans" then
+    return pkg.mkLibTarget lib
+  else if facet == "static" then
+    return pkg.mkStaticLibTarget lib |>.withoutInfo
+  else if facet == "shared" then
+    return pkg.mkSharedLibTarget lib |>.withoutInfo
+  else
+    throw <| CliError.unknownFacet "library" facet
+
+def resolveExeTarget (pkg : Package) (exe : LeanExeConfig) (facet : String) : Except CliError OpaqueTarget :=
+  if facet.isEmpty || facet == "exe" then
+    return pkg.mkExeTarget exe |>.withoutInfo
+  else
+    throw <| CliError.unknownFacet "executable" facet
+
+def resolvePackageTarget (pkg : Package) (facet : String) : Except CliError OpaqueTarget :=
+  if facet.isEmpty then
+    return pkg.defaultTarget
+  else if facet == "exe" || facet == "bin" then
+    return pkg.exeTarget.withoutInfo
+  else if facet == "staticLib" then
+    return pkg.staticLibTarget.withoutInfo
+  else if facet == "sharedLib" then
+    return pkg.sharedLibTarget.withoutInfo
+  else if facet == "leanLib" || facet == "oleans" then
+    return pkg.libTarget.withoutInfo
+  else
+    throw <| CliError.unknownFacet "package" facet
+
+def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Except CliError OpaqueTarget := do
   match spec.splitOn "/" with
-  | [pkgStr] =>
-    return (← parsePkgSpec ws pkgStr, none)
-  | [pkgStr, modStr] =>
-    let mod := modStr.toName
-    let pkg ← parsePkgSpec ws pkgStr
-    if pkg.hasModule mod then
-      return (pkg, mod)
+  | [spec] =>
+    if spec.isEmpty || spec.startsWith "@" then
+      let pkg ← parsePkgSpec ws <| spec.drop 1
+      resolvePackageTarget pkg facet
+    else if spec.startsWith "+" then
+      let mod := spec.drop 1 |>.toName
+      if let some pkg := ws.packageForModule? mod then
+        resolveModuleTarget pkg mod facet
+      else
+        throw <| CliError.unknownModule mod
+    else
+      if let some (pkg, exe) := ws.findExe? spec then
+        resolveExeTarget pkg exe facet
+      else if let some (pkg, lib) := ws.findLib? spec then
+        resolveLibTarget pkg lib facet
+      else if let some pkg := ws.packageByName? spec then
+        resolvePackageTarget pkg facet
+      else if let some pkg := ws.packageForModule? spec then
+        resolveModuleTarget pkg spec facet
+      else
+        throw <| CliError.unknownTarget spec
+  | [pkgSpec, targetSpec] =>
+    let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec
+    let pkg ← parsePkgSpec ws pkgSpec
+    if targetSpec.startsWith "+" then
+      let mod := targetSpec.drop 1 |>.toName
+      resolveModuleTarget pkg mod facet
     else
-      throw <| CliError.missingModule pkgStr modStr
+      if let some exe := pkg.findExe? spec then
+        resolveExeTarget pkg exe facet
+      else if let some lib := pkg.findLib? spec then
+        resolveLibTarget pkg lib facet
+      else if pkg.hasModule spec then
+        resolveModuleTarget pkg spec facet
+      else
+        throw <| CliError.missingTarget pkg.name targetSpec
   | _ =>
     throw <| CliError.invalidTargetSpec spec '/'
 
-def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError (BuildTarget PUnit) := do
+def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError OpaqueTarget := do
   match spec.splitOn ":" with
-  | [rootSpec] =>
-    let (pkg, mod?) ← parseTargetBaseSpec ws rootSpec
-    if let some mod := mod? then
-      return pkg.moduleOleanTarget mod |>.withoutInfo
-    else
-      return pkg.defaultTarget |>.withoutInfo
+  | [spec] =>
+    resolveTargetBaseSpec ws spec
   | [rootSpec, facet] =>
-    let (pkg, mod?) ← parseTargetBaseSpec ws rootSpec
-    if let some mod := mod? then
-      if facet == "olean" then
-        return pkg.moduleOleanTarget mod |>.withoutInfo
-      else if facet == "c" then
-        return pkg.moduleOleanAndCTarget mod |>.withoutInfo
-      else if facet == "o" then
-        return pkg.moduleOTarget mod |>.withoutInfo
-      else
-        throw <| CliError.unknownModuleFacet facet
-    else
-      if facet == "exe" || facet == "bin" then
-        return pkg.exeTarget.withoutInfo
-      else if facet == "staticLib" then
-        return pkg.staticLibTarget.withoutInfo
-      else if facet == "sharedLib" then
-        return pkg.sharedLibTarget.withoutInfo
-      else if facet == "oleans" then
-        return pkg.oleanTarget.withoutInfo
-      else
-        throw <| CliError.unknownPackageFacet  facet
+    resolveTargetBaseSpec ws rootSpec facet
   | _ =>
     throw <| CliError.invalidTargetSpec spec ':'
 
-def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (List (BuildTarget PUnit)) :=
+def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (List OpaqueTarget) :=
   specs.mapM <| parseTargetSpec ws
 
-def build (targets : List (BuildTarget PUnit)) : BuildM PUnit := do
+def build (targets : List OpaqueTarget) : BuildM PUnit := do
   let ws ← getWorkspace
   if targets.isEmpty then
     ws.root.defaultTarget.build

Diff for: Lake/CLI/Error.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 
 namespace Lake
+open Lean (Name)
 
 inductive CliError
 /- CLI Errors -/
@@ -16,10 +17,12 @@ inductive CliError
 | unknownLongOption (opt : String)
 | unexpectedArguments (args : List String)
 /- Build CLI Errors -/
+| unknownModule (mod : Name)
 | unknownPackage (spec : String)
-| unknownPackageFacet (spec : String)
-| unknownModuleFacet (spec : String)
-| missingModule (pkg mod : String)
+| unknownFacet (type facet : String)
+| unknownTarget (spec : String)
+| missingModule (pkg : Name) (mod : Name)
+| missingTarget (pkg : Name) (spec : String)
 | invalidTargetSpec (spec : String) (tooMany : Char)
 /- Script CLI Error -/
 | unknownScript (script : String)
@@ -41,10 +44,12 @@ def toString : CliError → String
 | unknownShortOption opt  => s!"unknown short option '-{opt}'"
 | unknownLongOption opt   => s!"unknown long option '{opt}'"
 | unexpectedArguments as  => s!"unexpected arguments: {" ".intercalate as}"
+| unknownModule mod       => s!"unknown module `{mod.toString false}`"
 | unknownPackage spec     => s!"unknown package `{spec}`"
-| unknownPackageFacet f   => s!"unknown package facet `{f}`"
-| unknownModuleFacet f    => s!"unknown module facet `{f}`"
-| missingModule pkg mod   => s!"package '{pkg}' has no module '{mod}'"
+| unknownFacet ty f       => s!"unknown {ty} facet `{f}`"
+| unknownTarget spec      => s!"unknown target `{spec}`"
+| missingModule pkg mod   => s!"package '{pkg.toString false}' has no module '{mod.toString false}'"
+| missingTarget pkg spec  => s!"package '{pkg.toString false}' has no target '{spec}'"
 | invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
 | unknownScript s         => s!"unknown script {s}"
 | missingScriptDoc s      => s!"no documentation provided for `{s}`"

Diff for: Lake/CLI/Help.lean

@@ -56,27 +56,36 @@ def helpBuild :=
 USAGE:
   lake build [<targets>...] [-- <args>...]
 
-A target is specified with a string of the form '<package>/<module>:<facet>'.
-The package must be the root package or one of its direct dependencies
-(i.e., those listed in the root configuration file).
+A target is specified with a string of the form:
+
+  [[@]<package>/][<target>|[+]<module>][:<facet>]
+
+The optional `@` and `+` markers can be used to disambiguate packages
+and modules from other kinds of targets (i.e., executables and libraries).
 
 PACKAGE FACETS:
-  bin                   build the package's binary
+  exe                   build the package's binary executable
+  leanLib               build the package's lean library (*.olean, *.ilean)
   staticLib             build the package's static library
   sharedLib             build the package's shared library
-  oleans                build the package's *.olean files
+
+LIBRARY FACETS:
+  lean                  build the library's lean binaries (*.olean, *.ilean)
+  static                build the library's static binary
+  shared                build the library's shared binary
 
 MODULE FACETS:
-  olean                 build the module's *.olean file
+  [default]             build the module's *.olean and *.ilean files
   c                     build the module's *.c file
   o                     build the module's *.o file
 
 TARGET EXAMPLES:
-  a                     build the default facet of package `a`
-  a/A                   build the .olean file of module `A` of package `a`
-  a/A:c                 build the .c file of module `A` of package `a`
-  a:oleans              build the olean files of package `a`
-  :bin                  build the root package's binary
+  a                     build the default facet of target `a`
+  +A                    build the .olean and .ilean files of module `A`
+  a/b                   build the default facet of target `b` of package `a`
+  a/+A:c                build the .c file of module `A` of package `a`
+  @a:leanLib            build the lean library of package `a`
+  :exe                  build the root package's executable
 
 A bare `build` command will build the default facet of the root package.
 Arguments to the `Packager` itself can be specified with `args`.

Diff for: Lake/Config/Package.lean

@@ -50,7 +50,8 @@ inductive PackageFacet
 | /-- The package's binary executable. **DEPRECATED:** Use `exe` instead. -/ bin
 | /-- The package's static library. -/ staticLib
 | /-- The package's shared library. -/ sharedLib
-| /-- The package's `.olean` files. -/ oleans
+| /-- The package's lean library (e.g. `olean` / `ilean` files). -/ leanLib
+| /-- The package's `.olean` files. **DEPRECATED:** Use `leanLib` instead. -/ oleans
 deriving BEq, DecidableEq, Repr
 instance : Inhabited PackageFacet := ⟨PackageFacet.bin⟩
 
@@ -216,6 +217,12 @@ structure PackageConfig extends WorkspaceConfig where
   -/
   moreLinkArgs : Array String := #[]
 
+  /-- Additional library targets for the package. -/
+  libConfigs : NameMap LeanLibConfig := {}
+
+  /-- Additional binary executable targets for the package. -/
+  exeConfigs : NameMap LeanExeConfig := {}
+
 deriving Inhabited
 
 namespace PackageConfig
@@ -305,9 +312,25 @@ def extraDepTarget (self : Package) : OpaqueTarget :=
 def defaultFacet (self : Package) : PackageFacet :=
    self.config.defaultFacet
 
+/-- The package's `libConfigs` configuration. -/
+def libConfigs (self : Package) : NameMap LeanLibConfig :=
+  self.config.libConfigs
+
+/-- Get the package's library configuration with the given name. -/
+def findLib? (self : Package) (name : Name) : Option LeanLibConfig :=
+  self.libConfigs.find? name
+
+/-- The package's `exeConfigs` configuration. -/
+def exeConfigs (self : Package) : NameMap LeanExeConfig :=
+  self.config.exeConfigs
+
+/-- Get the package's executable configuration with the given name. -/
+def findExe? (self : Package) (name : Name) : Option LeanExeConfig :=
+  self.exeConfigs.find? name
+
 /-- The package's `moreServerArgs` configuration. -/
 def moreServerArgs (self : Package) : Array String :=
-   self.config.moreServerArgs
+  self.config.moreServerArgs
 
 /-- The package's `dir` joined with its `srcDir` configuration. -/
 def srcDir (self : Package) : FilePath :=
@@ -395,8 +418,12 @@ def getModuleArray (self : Package) : IO (Array Name) :=
 
 /-- Whether the given module is considered local to the package. -/
 def isLocalModule (mod : Name) (self : Package) : Bool :=
+  self.libConfigs.any (fun _ lib => lib.isLocalModule mod) ||
   self.builtinLibConfig.isLocalModule mod
 
-/-- Whether the given module is in the package. -/
+/-- Whether the given module is in the package (i.e., can build it). -/
 def hasModule (mod : Name) (self : Package) : Bool :=
-  self.config.binRoot == mod || self.config.libGlobs.any fun glob => glob.matches mod
+  self.libConfigs.any (fun _ lib => lib.hasModule mod) ||
+  self.exeConfigs.any (fun _ exe => exe.root == mod) ||
+  self.builtinLibConfig.hasModule mod ||
+  self.config.binRoot == mod

Diff for: Lake/Config/Targets.lean

@@ -59,6 +59,10 @@ def isLocalModule (mod : Name) (self : LeanLibConfig) : Bool :=
   self.roots.any (fun root => root.isPrefixOf mod) ||
   self.globs.any (fun glob => glob.matches mod)
 
+/-- Whether the given module is in the library (i.e., is built as part of it). -/
+def hasModule (mod : Name) (self : LeanLibConfig) : Bool :=
+  self.globs.any fun glob => glob.matches mod
+
 /-- Get an `Array` of the library's modules. -/
 def getModuleArray (self : LeanLibConfig) (srcDir : FilePath) : IO (Array Name) := do
   let mut mods := #[]

Diff for: Lake/Config/Workspace.lean

@@ -95,6 +95,14 @@ def isLocalModule (mod : Name) (self : Workspace) : Bool :=
 def packageForModule? (mod : Name) (self : Workspace) : Option Package :=
   self.findPackage? (·.isLocalModule mod)
 
+/-- Get the workspace's library configuration with the given name. -/
+def findLib? (name : Name) (self : Workspace) : Option (Package × LeanLibConfig) :=
+  self.packageArray.findSome? fun pkg => pkg.findLib? name <&> (pkg, ·)
+
+/-- Get the workspace's executable configuration with the given name. -/
+def findExe? (name : Name) (self : Workspace) : Option (Package × LeanExeConfig) :=
+  self.packageArray.findSome? fun pkg => pkg.findExe? name <&> (pkg, ·)
+
 /-- The `LEAN_PATH` of the workspace. -/
 def oleanPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.oleanDir)

Diff for: examples/Makefile

@@ -3,10 +3,10 @@ LAKE ?= ../build/bin/lake
 all: check-lake test time-bootstrap check-bootstrap test-bootstrapped
 
 test: test-init test-hello test-io test-deps\
-	test-git test-ffi test-scripts
+	test-git test-ffi test-targets test-scripts
 
 clean: clean-init clean-hello clean-io clean-deps\
-	clean-git clean-ffi clean-bootstrap
+	clean-git clean-ffi clean-targets clean-bootstrap
 
 check-lake:
 	$(LAKE) self-check
@@ -47,6 +47,12 @@ test-ffi:
 clean-ffi:
 	cd ffi && ./clean.sh
 
+test-targets:
+	cd targets && ./test.sh
+
+clean-targets:
+	cd targets && ./clean.sh
+
 test-scripts:
 	cd scripts && ./test.sh
 

Diff for: examples/targets/.gitignore

@@ -0,0 +1 @@
+/build

Diff for: examples/targets/clean.sh

@@ -0,0 +1 @@
+rm -rf build