feat: lake: improve package templates

* add library directory
* add note on `supportInterpreter`
* use `where`-style configs

src/lake/Lake/CLI/Init.lean

@@ -22,9 +22,14 @@ s!"/{defaultBuildDir}
 /{defaultPackagesDir}/*
 "
 
-def libFileContents :=
+def basicFileContents :=
   s!"def hello := \"world\""
 
+def libRootFileContents (libName : String) (libRoot : String) :=
+s!"-- This module serves as the root of the `{libName}` library.
+-- Import modules here that should be built as part of the library.
+import {libRoot}.Basic"
+
 def mainFileName : FilePath :=
   s!"{defaultExeRoot}.lean"
 
@@ -44,63 +49,61 @@ def stdConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
-package {pkgName} \{
+package {pkgName} where
   -- add package configuration options here
-}
 
-lean_lib {libRoot} \{
+lean_lib {libRoot} where
   -- add library configuration options here
-}
 
 @[default_target]
-lean_exe {pkgName} \{
+lean_exe {pkgName} where
   root := `Main
-}
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true
 "
 
 def exeConfigFileContents (pkgName exeRoot : String) :=
 s!"import Lake
 open Lake DSL
 
-package {pkgName} \{
+package {pkgName} where
   -- add package configuration options here
-}
 
 @[default_target]
-lean_exe {exeRoot} \{
-  -- add executable configuration options here
-}
+lean_exe {exeRoot} where
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true
 "
 
 def libConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
-package {pkgName} \{
+package {pkgName} where
   -- add package configuration options here
-}
 
 @[default_target]
-lean_lib {libRoot} \{
+lean_lib {libRoot} where
   -- add library configuration options here
-}
 "
 
 def mathConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
-package {pkgName} \{
+package {pkgName} where
   -- add any package configuration options here
-}
 
 require mathlib from git
   \"https://github.com/leanprover-community/mathlib4.git\"
 
 @[default_target]
-lean_lib {libRoot} \{
+lean_lib {libRoot} where
   -- add any library configuration options here
-}
 "
 
 def mathToolchainUrl : String :=
@@ -164,9 +167,14 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En
     unless (← rootFile.pathExists) do
       IO.FS.writeFile rootFile exeFileContents
   else
-    if !rootExists then
-      IO.FS.createDirAll rootFile.parent.get!
-      IO.FS.writeFile rootFile libFileContents
+    unless rootExists do
+      let libDir := rootFile.withExtension ""
+      let basicFile := libDir / "Basic.lean"
+      unless (← basicFile.pathExists) do
+        IO.FS.createDirAll libDir
+        IO.FS.writeFile basicFile basicFileContents
+      let rootContents := libRootFileContents root.toString rootNameStr
+      IO.FS.writeFile rootFile rootContents
     if tmp = .std then
       let mainFile := dir / mainFileName
       unless (← mainFile.pathExists) do

src/lake/Lake/Config/LeanExeConfig.lean

@@ -51,12 +51,13 @@ structure LeanExeConfig extends LeanConfig where
   nativeFacets : Array (ModuleFacet (BuildJob FilePath)) := #[Module.oFacet]
 
   /--
-  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`).
+  Enables the executable to interpret Lean files (e.g., via
+  `Lean.Elab.runFrontend`) by exposing symbols within the  executable
+  to the Lean interpreter.
 
   Implementation-wise, this passes `-rdynamic` to the linker when building
-  on non-Windows systems.
+  on non-Windows systems. This increases the size of the binary on Linux, so
+  this feature should only be enabled when necessary.
 
   Defaults to `false`.
   -/

src/lake/tests/clone/test.sh

@@ -44,7 +44,7 @@ $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
 # Test that Lake produces a warning if local changes are made to a dependency
 # See https://github.com/leanprover/lake/issues/167
 
-sed_i "s/world/changes/" lake-packages/hello/Hello.lean
+sed_i "s/world/changes/" lake-packages/hello/Hello/Basic.lean
 ! git -C lake-packages/hello diff --exit-code
 $LAKE build 3>&1 1>&2 2>&3 | grep "has local changes"
 ./build/bin/test | grep "Hello, changes"

src/lake/tests/init/test.sh

@@ -7,23 +7,25 @@ LAKE=${LAKE:-../../build/bin/lake}
 
 # Test `new` and `init` with bad template (should error)
 
-$LAKE new foo bar && exit 1 || true
-$LAKE init foo bar && exit 1 || true
+! $LAKE new foo bar
+! $LAKE init foo bar
 
-# Test `new` with `.`
+# Test creating multi-level packages with a `.`
 
 $LAKE new hello.world
 $LAKE -d hello-world build
 hello-world/build/bin/hello-world
+test -f hello-world/Hello/World/Basic.lean
 
-# Test `new` with `-`
+# Test creating packages with a `-` (i.e., a non-Lean name)
 # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20new.20lean-data
 
 $LAKE new lean-data
 $LAKE -d lean-data build
 lean-data/build/bin/lean-data
 
-# Test issue 128
+# Test creating packages with keyword names
+# https://github.com/leanprover/lake/issues/128
 
 $LAKE new meta
 $LAKE -d meta build