chore: remove package config builtin targets

Lake/Build/Index.lean

@@ -122,23 +122,14 @@ export BuildInfo (build buildIn)
 @[inline] protected def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
   self.lean.target
 
-@[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget :=
-  self.builtinLib.leanTarget
-
 /-! ### Native Lean Lib Targets -/
 
 @[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
   self.static.target.withInfo self.sharedLibFile
 
-@[inline] protected def Package.staticLibTarget (self : Package) : FileTarget :=
-  self.builtinLib.staticLibTarget
-
 @[inline] protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget :=
   self.shared.target.withInfo self.sharedLibFile
 
-@[inline] protected def Package.sharedLibTarget (self : Package) : FileTarget :=
-  self.builtinLib.sharedLibTarget
-
 /-! ### Lean Executable Targets -/
 
 @[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget :=
@@ -149,6 +140,3 @@ export BuildInfo (build buildIn)
 
 @[inline] protected def LeanExe.target (self : LeanExe) : FileTarget :=
   self.exe.target.withInfo self.file
-
-@[inline] protected def Package.exeTarget (self : Package) : FileTarget :=
-  self.builtinExe.target

Lake/CLI/Build.lean

@@ -8,14 +8,6 @@ import Lake.CLI.Error
 
 namespace Lake
 
-def Package.defaultTarget (self : Package) : OpaqueTarget :=
-  match self.defaultFacet with
-  | .exe => self.exeTarget.withoutInfo
-  | .staticLib => self.staticLibTarget.withoutInfo
-  | .sharedLib => self.sharedLibTarget.withoutInfo
-  | .leanLib => self.leanLibTarget.withoutInfo
-  | .none => Target.nil
-
 def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package :=
   if spec.isEmpty then
     return ws.root
@@ -86,23 +78,12 @@ def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (fac
     throw <| CliError.missingTarget pkg.name (target.toString false)
 
 def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError OpaqueTarget :=
-  if pkg.defaultTargets.isEmpty then
-    return pkg.defaultTarget
-  else
-    return Target.collectOpaqueArray <| ←
-      pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous)
+  return Target.collectOpaqueArray <| ←
+    pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous)
 
 def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError OpaqueTarget :=
   if facet.isAnonymous then
     resolveDefaultPackageTarget ws pkg
-  else if facet == `exe 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 then
-    return pkg.leanLibTarget.withoutInfo
   else if let some config := ws.findPackageFacetConfig? facet then do
     let some target := config.toTarget? (pkg.facet facet) rfl
       | throw <| CliError.nonTargetFacet "package" facet

Lake/CLI/Init.lean

@@ -11,6 +11,9 @@ import Lake.Load.Config
 namespace Lake
 open Git System
 
+/-- The default module of an executable in `std` package. -/
+def defaultExeRoot : Name := `Main
+
 /-- `elan` toolchain file name -/
 def toolchainFileName : FilePath :=
   "lean-toolchain"
@@ -25,7 +28,7 @@ def libFileContents :=
   s!"def hello := \"world\""
 
 def mainFileName : FilePath :=
-  s!"{defaultBinRoot}.lean"
+  s!"{defaultExeRoot}.lean"
 
 def mainFileContents (libRoot : Name) :=
 s!"import {libRoot}

Lake/Config/LeanExe.lean

@@ -20,10 +20,6 @@ structure LeanExe where
 @[inline] def Package.leanExes (self : Package) : Array LeanExe :=
   self.leanExeConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[]
 
-/-- The Lean executable built into the package. -/
-@[inline] def Package.builtinExe (self : Package) : LeanExe :=
-  ⟨self, self.builtinExeConfig⟩
-
 /-- Try to find a Lean executable in the package with the given name. -/
 @[inline] def Package.findLeanExe? (name : Name) (self : Package) : Option LeanExe :=
   self.leanExeConfigs.find? name |>.map (⟨self, ·⟩)
@@ -86,6 +82,4 @@ end LeanExe
 /-- Locate the named module in the package (if it is buildable and local to it). -/
 def Package.findModule? (mod : Name) (self : Package) : Option Module :=
   self.leanLibs.findSome? (·.findModule? mod) <|>
-  self.leanExes.findSome? (·.isRoot? mod) <|>
-  self.builtinLib.findModule? mod <|>
-  self.builtinExe.isRoot? mod
+  self.leanExes.findSome? (·.isRoot? mod)

Lake/Config/LeanLib.lean

@@ -20,10 +20,6 @@ structure LeanLib where
 @[inline] def Package.leanLibs (self : Package) : Array LeanLib :=
   self.leanLibConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[]
 
-/-- The Lean library built into the package. -/
-@[inline] def Package.builtinLib (self : Package) : LeanLib :=
-  ⟨self, self.builtinLibConfig⟩
-
 /-- Try to find a Lean library in the package with the given name. -/
 @[inline] def Package.findLeanLib? (name : Name) (self : Package) : Option LeanLib :=
   self.leanLibConfigs.find? name |>.map (⟨self, ·⟩)

Lake/Config/Package.lean

@@ -35,23 +35,6 @@ def defaultOleanDir : FilePath := defaultLibDir
 /-- The default setting for a `PackageConfig`'s `irDir` option. -/
 def defaultIrDir : FilePath := "ir"
 
-/-- The default setting for a `PackageConfig`'s `binRoot` option. -/
-def defaultBinRoot : Name := `Main
-
---------------------------------------------------------------------------------
-/-! # PackageFacet -/
---------------------------------------------------------------------------------
-
-/-- A buildable component of a `Package`. -/
-inductive PackageFacet
-| /-- The package's binary executable. -/ exe
-| /-- The package's static library. -/ staticLib
-| /-- The package's shared library. -/ sharedLib
-| /-- The package's lean library (e.g. `olean` / `ilean` files). -/ leanLib
-| /-- The package has no buildable component. -/ none
-deriving BEq, DecidableEq, Repr
-instance : Inhabited PackageFacet := ⟨PackageFacet.exe⟩
-
 --------------------------------------------------------------------------------
 /-! # PackageConfig -/
 --------------------------------------------------------------------------------
@@ -72,17 +55,6 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   -/
   extraDepTarget : Option OpaqueTarget := none
 
-  /--
-  The optional `PackageFacet` to build on a bare `lake build` of the package.
-  Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`, or `none`.
-  Defaults to `exe`. See `lake help build` for more info on build facets.
-
-  **DEPRECATED:**
-  Package facets will be removed in a future version of Lake.
-  Use a separate `lean_lib` or `lean_exe` default target instead.
-  -/
-  defaultFacet : PackageFacet := .exe
-
   /--
   Whether to compile each of the package's module into a native shared library
   that is loaded whenever the module is imported. This speeds up evaluation of
@@ -128,26 +100,6 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   -/
   oleanDir : FilePath := defaultOleanDir
 
-  /--
-  The root module(s) of the package's library.
-
-  Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered
-  part of the package.
-
-  Defaults to a single root of the package's upper camel case `name`.
-  -/
-  libRoots : Array Name := #[toUpperCamelCase name]
-
-  /--
-  An `Array` of module `Glob`s to build for the package's library.
-  Defaults to a `Glob.one` of each of the module's `libRoots`.
-
-  Submodule globs build every source file within their directory.
-  Local imports of glob'ed files (i.e., fellow modules of the package) are
-  also recursively built.
-  -/
-  libGlobs : Array Glob := libRoots.map Glob.one
-
   /--
   The build subdirectory to which Lake should output
   the package's intermediary results (e.g., `.c` and `.o` files).
@@ -155,85 +107,20 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   -/
   irDir : FilePath := defaultIrDir
 
-  /--
-  The name of the package's static library.
-  Defaults to the package's upper camel case `name`.
-  -/
-  libName : String := toUpperCamelCase name |>.toString (escape := false)
-
   /--
   The build subdirectory to which Lake should output the package's static library.
   Defaults to `defaultLibDir` (i.e., `lib`).
   -/
   libDir : FilePath := defaultLibDir
 
-  /--
-  The name of the package's binary executable.
-  Defaults to the package's `name` with any `.` replaced with a `-`.
-  -/
-  binName : String := name.toStringWithSep "-" (escape := false)
-
   /--
   The build subdirectory to which Lake should output the package's binary executable.
   Defaults to `defaultBinDir` (i.e., `bin`).
   -/
   binDir : FilePath := defaultBinDir
 
-  /--
-  The root module of the package's binary executable.
-  Defaults to `defaultBinRoot` (i.e., `Main`).
-
-  The root is built by recursively building its
-  local imports (i.e., fellow modules of the workspace).
-
-  This setting is most useful for packages that are distributing both a
-  library and a binary (like Lake itself). In such cases, it is common for
-  there to be code (e.g., `main`) that is needed for the binary but should
-  not be included in the library proper.
-  -/
-  binRoot : Name := defaultBinRoot
-
-  /--
-  Additional library `FileTarget`s (beyond the package's and its dependencies'
-  Lean libraries) to build and link to the package's binaries (and to dependent
-  packages' binaries).
-
-  **DEPRECATED:** Use separate `extern_lib` targets instead.
-  -/
-  moreLibTargets : Array FileTarget := #[]
-
-  /--
-  Whether to expose symbols within the executable to the Lean interpreter.
-  This allows the executable to interpret Lean files (e.g.,  via
-  `Lean.Elab.runFrontend`).
-
-  Implementation-wise, this passes `-rdynamic` to the linker when building
-  on non-Windows systems.
-
-  Defaults to `false`.
-  -/
-  supportInterpreter : Bool := false
-
 deriving Inhabited
 
-namespace PackageConfig
-
-/-- The configuration of the package's library. -/
-def toLeanLibConfig (self : PackageConfig) : LeanLibConfig where
-  name := self.libName
-  roots := self.libRoots
-  globs := self.libGlobs
-  toLeanConfig := self.toLeanConfig
-
-/-- The configuration of the package's binary executable. -/
-def toLeanExeConfig (self : PackageConfig) : LeanExeConfig where
-  root := self.binRoot
-  name := self.binName
-  supportInterpreter := self.supportInterpreter
-  toLeanConfig := self.toLeanConfig
-
-end PackageConfig
-
 --------------------------------------------------------------------------------
 /-! # Package -/
 --------------------------------------------------------------------------------
@@ -289,10 +176,6 @@ namespace Package
 @[inline] def extraDepTarget (self : Package) : OpaqueTarget :=
   self.config.extraDepTarget.getD Target.nil
 
-/-- The package's `defaultFacet` configuration. -/
-@[inline] def defaultFacet (self : Package) : PackageFacet :=
-   self.config.defaultFacet
-
 /-- The package's `precompileModules` configuration. -/
 @[inline] def precompileModules (self : Package) : Bool :=
   self.config.precompileModules
@@ -349,25 +232,14 @@ namespace Package
 @[inline] def binDir (self : Package) : FilePath :=
   self.buildDir / self.config.binDir
 
-/-- The library configuration built into the package configuration. -/
-@[inline] def builtinLibConfig (self : Package) : LeanLibConfig :=
-  self.config.toLeanLibConfig
-
-/-- The binary executable configuration built into the package configuration. -/
-@[inline] def builtinExeConfig (self : Package) : LeanExeConfig :=
-  self.config.toLeanExeConfig
-
 /-- Whether the given module is considered local to the package. -/
 def isLocalModule (mod : Name) (self : Package) : Bool :=
-  self.leanLibConfigs.any (fun _ lib => lib.isLocalModule mod) ||
-  self.builtinLibConfig.isLocalModule mod
+  self.leanLibConfigs.any (fun _ lib => lib.isLocalModule mod)
 
 /-- Whether the given module is in the package (i.e., can build it). -/
 def isBuildableModule (mod : Name) (self : Package) : Bool :=
   self.leanLibConfigs.any (fun _ lib => lib.isBuildableModule mod) ||
-  self.leanExeConfigs.any (fun _ exe => exe.root == mod) ||
-  self.builtinLibConfig.isBuildableModule mod ||
-  self.config.binRoot == mod
+  self.leanExeConfigs.any (fun _ exe => exe.root == mod)
 
 /-- Remove the package's build outputs (i.e., delete its build directory). -/
 def clean (self : Package) : IO PUnit := do

Lake/Load/Package.lean

@@ -80,9 +80,6 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
   if self.config.extraDepTarget.isSome then
     logWarning <| "`extraDepTarget` has been deprecated. " ++
       "Try to use a custom target or raise an issue about your use case."
-  if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && self.defaultFacet ≠ .none then
-    logWarning <| "Package targets are deprecated. " ++
-      "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
 
   -- Fill in the Package
   return {self with

examples/hello/lakefile.lean

@@ -3,6 +3,8 @@ open Lake DSL
 
 package hello
 
+lean_lib Hello
+
 @[defaultTarget]
 lean_exe hello {
   root := `Main

examples/scripts/lakefile.lean

@@ -1,8 +1,7 @@
 import Lake
 open Lake DSL
 
-package scripts where
-  defaultFacet := .none
+package scripts
 
 /--
 Display a greeting

test/62/test.sh

@@ -5,8 +5,8 @@ set -euxo pipefail
 command -v elan > /dev/null || (echo "elan not found; skipping test"; exit 0)
 
 ./clean.sh
-lake +leanprover/lean4:4.0.0-m3 new foo
+lake +leanprover/lean4:nightly-2022-06-30 new foo
 cd foo
-lake +leanprover/lean4:4.0.0-m3 build | grep -m1 foo
+lake +leanprover/lean4:nightly-2022-06-30 build | grep -m1 foo
 cp ../../../lean-toolchain lean-toolchain
 ${LAKE:-../../../build/bin/lake} build | grep -m1 foo