diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index 1a05418..a520625 100644
--- a/Lake/Build/Package.lean
+++ b/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)
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index 3c4f893..3b327e6 100644
--- a/Lake/CLI/Build.lean
+++ b/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
diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean
index 3a71a93..47a38e6 100644
--- a/Lake/CLI/Init.lean
+++ b/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!
diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean
index 7b6681d..01e9f07 100644
--- a/Lake/Config/Load.lean
+++ b/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"
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index dae17c8..24d9132 100644
--- a/Lake/Config/Package.lean
+++ b/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
diff --git a/examples/bootstrap/lakefile.lean b/examples/bootstrap/lakefile.lean
index 0c364f5..2403582 100644
--- a/examples/bootstrap/lakefile.lean
+++ b/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
diff --git a/examples/deps/a/lakefile.lean b/examples/deps/a/lakefile.lean
index bfc9d12..ecf4166 100644
--- a/examples/deps/a/lakefile.lean
+++ b/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
diff --git a/examples/deps/b/lakefile.lean b/examples/deps/b/lakefile.lean
index ae01b2b..784d438 100644
--- a/examples/deps/b/lakefile.lean
+++ b/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
diff --git a/examples/deps/bar/lakefile.lean b/examples/deps/bar/lakefile.lean
index 59227dd..c461c85 100644
--- a/examples/deps/bar/lakefile.lean
+++ 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
diff --git a/examples/deps/foo/lakefile.lean b/examples/deps/foo/lakefile.lean
index 0a7168d..9be985a 100644
--- a/examples/deps/foo/lakefile.lean
+++ b/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
diff --git a/examples/deps/root/lakefile.lean b/examples/deps/root/lakefile.lean
index eebdec9..8b0268d 100644
--- a/examples/deps/root/lakefile.lean
+++ b/examples/deps/root/lakefile.lean
@@ -1,3 +1,5 @@
 import Lake
 open Lake DSL
+
 package root
+@[defaultTarget] lean_lib Root
diff --git a/examples/ffi/app/Main.lean b/examples/ffi/app/Main.lean
index 865c82a..e763be6 100644
--- a/examples/ffi/app/Main.lean
+++ b/examples/ffi/app/Main.lean
@@ -1,4 +1,4 @@
-import Ffi
+import FFI
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2
diff --git a/examples/ffi/app/lakefile.lean b/examples/ffi/app/lakefile.lean
index 8f6704e..d4f6f28 100644
--- a/examples/ffi/app/lakefile.lean
+++ b/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
+}
diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean
index 8e6b0bd..edd136e 100644
--- a/examples/ffi/lib/lakefile.lean
+++ b/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
+}
diff --git a/examples/ffi/lib/lean/FFI.lean b/examples/ffi/lib/lean/FFI.lean
new file mode 100644
index 0000000..9ba9956
--- /dev/null
+++ b/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
diff --git a/examples/ffi/lib/lean/Main.lean b/examples/ffi/lib/lean/Main.lean
index 865c82a..e763be6 100644
--- a/examples/ffi/lib/lean/Main.lean
+++ b/examples/ffi/lib/lean/Main.lean
@@ -1,4 +1,4 @@
-import Ffi
+import FFI
 
 def main : IO Unit :=
   IO.println <| myAdd 1 2
diff --git a/examples/ffi/test.sh b/examples/ffi/test.sh
index a295950..4cc7907 100755
--- a/examples/ffi/test.sh
+++ b/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
diff --git a/examples/git/lakefile.lean b/examples/git/lakefile.lean
index 64aee55..1674e9f 100644
--- a/examples/git/lakefile.lean
+++ b/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
+}
diff --git a/examples/hello/lakefile.lean b/examples/hello/lakefile.lean
index 5506099..d51a593 100644
--- a/examples/hello/lakefile.lean
+++ b/examples/hello/lakefile.lean
@@ -1,5 +1,9 @@
 import Lake
 open Lake DSL
 
-package hello {
+package hello
+
+@[defaultTarget]
+lean_exe hello {
+  root := `Main
 }