chore: deprecate package facets

Lake/Build/Package.lean

@@ -90,8 +90,9 @@ def Workspace.processImportList
 /--
 Build the workspace-local modules of list of imports.
 
-Builds only module `.olean` files if the default package facet is
-just `oleans`. Otherwise, builds both `.olean` and `.c` files.
+Build only module `.olean` and `.ilean` files if the default package facet is
+just `leanLib` or `oleans` (and the package has no binary executable targets).
+Otherwise, also build `.c` files.
 -/
 def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
   let depTarget ← self.buildExtraDepsTarget
@@ -101,7 +102,7 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
   else
     -- build local imports from list
     let infos := (← getWorkspace).processImportList imports
-    if self.defaultFacet == PackageFacet.oleans then
+    if (self.defaultFacet == .leanLib || self.defaultFacet == .oleans) && self.exes.isEmpty then
       let build := recBuildModuleOleanTargetWithLocalImports depTarget
       let targets ← buildModuleArray infos build
       targets.forM (·.buildOpaque)

Lake/CLI/Build.lean

@@ -12,12 +12,10 @@ namespace Lake
 
 def Package.defaultTarget (self : Package) : OpaqueTarget :=
   match self.defaultFacet with
-  | .exe => self.exeTarget.withoutInfo
-  | .bin => self.exeTarget.withoutInfo
+  | .exe | .bin => self.exeTarget.withoutInfo
   | .staticLib => self.staticLibTarget.withoutInfo
   | .sharedLib => self.sharedLibTarget.withoutInfo
-  | .leanLib => self.libTarget.withoutInfo
-  | .oleans => self.libTarget.withoutInfo
+  | .leanLib | .oleans => self.libTarget.withoutInfo
 
 def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package :=
   if spec.isEmpty then

Lake/CLI/Init.lean

@@ -35,27 +35,37 @@ def main : IO Unit :=
   IO.println s!\"Hello, \{hello}!\"
 "
 
-def pkgConfigFileContents (pkgName : String) :=
+def pkgConfigFileContents (pkgName : Name) (libRoot : Name) :=
 s!"import Lake
 open Lake DSL
 
-package {pkgName.toName} \{
-  -- add configuration options here
+package {pkgName} \{
+  -- add package configuration options here
+}
+
+lean_lib {libRoot} \{
+  -- add library configuration options here
+}
+
+@[defaultTarget]
+lean_exe {pkgName} \{
+  root := `Main
 }
 "
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
 def initPkg (dir : FilePath) (name : String) : IO PUnit := do
+  let pkgName := name.decapitalize.toName
+  let libRoot := toUpperCamelCase name.toName
 
   -- write default configuration file
   let configFile := dir / defaultConfigFile
   if (← configFile.pathExists) then
     -- error if package already has a `lakefile.lean`
     throw <| IO.userError "package already initialized"
-  IO.FS.writeFile configFile (pkgConfigFileContents name)
+  IO.FS.writeFile configFile (pkgConfigFileContents pkgName libRoot)
 
   -- write example code if the files do not already exist
-  let libRoot := toUpperCamelCase name.toName
   let libFile := Lean.modToFilePath dir libRoot "lean"
   unless (← libFile.pathExists) do
     IO.FS.createDirAll libFile.parent.get!

Lake/Config/Load.lean

@@ -111,6 +111,9 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
       let exes ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d =>
         let eval := env.evalConstCheck LeanExeConfig leanOpts ``LeanExeConfig d
         return m.insert d <| ← IO.ofExcept eval.run.run
+      if libs.isEmpty && exes.isEmpty then
+        logWarning <| "Package targets are deprecated. " ++
+          "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
       let defaultTargets := defaultTargetAttr.ext.getState env |>.toArray
       return {dir, config, scripts, libs, exes, defaultTargets}
     | _ => error s!"configuration file has multiple `package` declarations"

Lake/Config/Package.lean

@@ -53,7 +53,7 @@ inductive PackageFacet
 | /-- 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⟩
+instance : Inhabited PackageFacet := ⟨PackageFacet.exe⟩
 
 --------------------------------------------------------------------------------
 -- # PackageConfig
@@ -80,11 +80,15 @@ structure PackageConfig extends WorkspaceConfig where
   extraDepTarget : OpaqueTarget := Target.nil
 
   /--
-  The `PackageFacet` to build on a bare `lake build` of the package.
-  Can be one of `exe` (or `bin`), `staticLib`, `sharedLib`, or `oleans`.
+  The optional `PackageFacet` to build on a bare `lake build` of the package.
+  Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`.
   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 := PackageFacet.exe
+  defaultFacet : PackageFacet := .exe
 
   /--
   Additional arguments to pass to the Lean language server

examples/bootstrap/lakefile.lean

@@ -2,6 +2,11 @@ import Lake
 open System Lake DSL
 
 package lake where
-  srcDir := FilePath.mk ".." / ".."
-  binRoot := `Lake.Main
+  srcDir := ".." / ".."
+
+lean_lib Lake
+
+@[defaultTarget]
+lean_exe lake where
+  root := `Lake.Main
   supportInterpreter := true

examples/deps/a/lakefile.lean

@@ -1,6 +1,6 @@
 import Lake
 open System Lake DSL
 
-require root from ".."/"root"
-
 package a
+require root from ".."/"root"
+@[defaultTarget] lean_lib A

examples/deps/b/lakefile.lean

@@ -1,6 +1,6 @@
 import Lake
 open System Lake DSL
 
-require root from ".."/"root"
-
 package b
+require root from ".."/"root"
+@[defaultTarget] lean_lib B

examples/deps/bar/lakefile.lean

@@ -1,6 +1,12 @@
 import Lake
 open System Lake DSL
 
+package bar
+
 require foo from ".."/"foo"
 
-package bar
+lean_lib Bar
+
+@[defaultTarget]
+lean_exe bar where
+  root := `Main

examples/deps/foo/lakefile.lean

@@ -1,7 +1,13 @@
 import Lake
 open System Lake DSL
 
+package foo
+
 require a from ".."/"a"
 require b from ".."/"b"
 
-package foo
+lean_lib Foo
+
+@[defaultTarget]
+lean_exe foo where
+  root := `Main

examples/deps/root/lakefile.lean

@@ -1,3 +1,5 @@
 import Lake
 open Lake DSL
+
 package root
+@[defaultTarget] lean_lib Root

examples/ffi/app/Main.lean

@@ -1,4 +1,4 @@
-import Ffi
+import FFI
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2

examples/ffi/app/lakefile.lean

@@ -1,5 +1,11 @@
 import Lake
 open System Lake DSL
 
-require ffi from ".."/"lib"
 package app
+
+require ffi from ".."/"lib"
+
+@[defaultTarget]
+lean_exe app {
+  root := `Main
+}

examples/ffi/lib/lakefile.lean

@@ -18,7 +18,12 @@ def cLibTarget (pkgDir : FilePath) : FileTarget :=
 package ffi {
   -- customize layout
   srcDir := "lean"
-  libRoots := #[`Ffi]
   -- specify the lib as an additional target
   moreLibTargets := #[cLibTarget __dir__]
 }
+
+lean_lib FFI
+
+@[defaultTarget] lean_exe test {
+  root := `Main
+}

examples/ffi/lib/lean/FFI.lean

@@ -0,0 +1,5 @@
+@[extern "my_add"]
+constant myAdd : UInt32 → UInt32 → UInt32
+
+@[extern "my_lean_fun"]
+constant myLeanFun : IO PUnit

examples/ffi/lib/lean/Main.lean

@@ -1,4 +1,4 @@
-import Ffi
+import FFI
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2

examples/ffi/test.sh

@@ -3,4 +3,4 @@ set -e
 ./clean.sh
 ./package.sh
 ./app/build/bin/app
-./lib/build/bin/ffi
+./lib/build/bin/test

examples/git/lakefile.lean

@@ -2,7 +2,12 @@ import Lake
 import Lean.Meta
 open System Lake DSL
 
+package git_hello
+
 require hello from git
   "https://github.com/leanprover/lake.git"@"master"/"examples"/"hello"
 
-package git_hello
+@[defaultTarget]
+lean_exe git_hello {
+  root := `Main
+}

examples/hello/lakefile.lean

@@ -1,5 +1,9 @@
 import Lake
 open Lake DSL
 
-package hello {
+package hello
+
+@[defaultTarget]
+lean_exe hello {
+  root := `Main
 }