fix: lake: no lib files for exe template (#14366)

This PR fixes `lake new` and `lake init` to not emit library files on
the `exe` template. It also fixes a related bug where the commands could
sometimes overwrite library files for existing packages.

These bugs were introduced in v4.10 with #2439. To prevent regressions,
the `init` test has been updated to better validate the file structure
produced by each template.

Closes #11671

Author: tydeu

src/lake/Lake/CLI/Init.lean

@@ -420,7 +420,7 @@ def initPkg
     let root := name
     let rootFile := Lean.modToFilePath dir root "lean"
     if tmp = .exe || (← rootFile.pathExists) then
-      return (root, some rootFile)
+      return (root, none)
     else
       let root := toUpperCamelCase name
       let rootFile := Lean.modToFilePath dir root "lean"

tests/lake/tests/init/test.sh

@@ -34,60 +34,77 @@ done
 
 # Test default (std) template
 
+test_std() {
+  local pkg=$1; local mod=$2; local exe=${3:-$1}
+  test_exp -f $pkg/Main.lean
+  test_exp -f $pkg/$mod.lean
+  test_exp -f $pkg/$mod/Basic.lean
+  test_run -d $pkg exe $exe
+  test_exp -f $pkg/.lake/build/lib/lean/$mod.olean
+}
+
 echo "# TEST: default template"
 test_run new hello .lean
-test_run -d hello exe hello
-test -f hello/.lake/build/lib/lean/Hello.olean
+test_std hello Hello
 rm -rf hello
 test_run new hello .toml
-test_run -d hello exe hello
-test -f hello/.lake/build/lib/lean/Hello.olean
+test_std hello Hello
 rm -rf hello
 
 # Test exe template
 
+test_exe() {
+  local pkg=$1; local mod=${2:-$1}; local exe=${3:-$1}
+  test_exp ! -d $pkg/$mod
+  test_exp -f $pkg/Main.lean
+  test_run -d $pkg exe $exe
+}
+
 echo "# TEST: exe template"
 test_run new hello exe.lean
-test -f hello/Main.lean
-test_run -d hello exe hello
+test_exe hello Hello
 rm -rf hello
 test_run new hello exe.toml
-test -f hello/Main.lean
-test_run -d hello exe hello
+test_exe hello Hello
 rm -rf hello
 
 # Test lib template
 
+test_lib() {
+  local pkg=$1; local mod=$2
+  test_exp -f $pkg/$mod.lean
+  test_exp -f $pkg/$mod/Basic.lean
+  test_exp ! -f $pkg/Main.lean
+  test_run -d $pkg build $mod
+  test_exp -f $pkg/.lake/build/lib/lean/$mod.olean
+}
+
 echo "# TEST: lib template"
 test_run new hello lib.lean
-test_run -d hello build Hello
-test -f hello/.lake/build/lib/lean/Hello.olean
+test_lib hello Hello
 rm -rf hello
 test_run new hello lib.toml
-test_run -d hello build Hello
-test -f hello/.lake/build/lib/lean/Hello.olean
+test_lib hello Hello
 rm -rf hello
 
 # Test math & math-lax template
 
 test_math_tmp () {
-  tmp=$1; pkg=$2; mod=$3
+  local tmp=$1; local pkg=$2; local mod=$3
   echo "# TEST: $tmp template"
   # Use `--offline` and remove the `require`,
   # since we do not wish to download mathlib during tests
   ELAN_TOOLCHAIN="v4.0.0-test" test_run new $pkg $tmp.lean --offline
   sed_i '/^require.*/{N;d;}' $pkg/lakefile.lean
   test_cmd_out "v4.0.0-test" cat $pkg/lean-toolchain
-  test_run -d $pkg build $mod
-  test -f $pkg/.lake/build/lib/lean/$mod.olean
+  test_lib $pkg $mod
   rm -rf $pkg
   # Use `--offline` and remove the `require`,
   # since we do not wish to download mathlib during tests
   test_out "creating a new math package with a non-release Lean toolchain" \
     new $pkg $tmp.toml --offline
   sed_i '/^\[\[require\]\]/{N;N;N;d;}' $pkg/lakefile.toml
-  test_run -d $pkg build $mod
-  test -f $pkg/.lake/build/lib/lean/$mod.olean
+  test_lib $pkg $mod
 }
 
 test_math_tmp math-lax qed-lax QedLax
@@ -99,39 +116,38 @@ echo "# TEST: init ."
 mkdir hello
 pushd hello
 test_run init .
-test_run exe hello
+test_std . Hello hello
 popd
 
 # Test creating packages with uppercase names
 # https://github.com/leanprover/lean4/issues/2540
 
 echo "# TEST: Uppercase package names"
 test_run new HelloWorld
-test_run -d HelloWorld exe helloworld
+test_std HelloWorld HelloWorld helloworld
 
 # Test creating multi-level packages with a `.`
 
 echo "# TEST: Packages with a `.`"
 test_run new hello.world
-test_run -d hello-world exe hello-world
-test -f hello-world/Hello/World/Basic.lean
+test_std hello-world Hello/World
 
 test_run new hello.exe exe
-test_run -d hello-exe exe hello-exe
+test_exe hello-exe Hello
 
 # Test creating packages with a `-` (i.e., a non-identifier package name)
 # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20new.20lean-data
 
 echo "# TEST: Non-identifier package names"
 test_run new lean-data
-test_run -d lean-data exe lean-data
+test_std lean-data LeanData
 
 # Test creating packages starting with digits (i.e., a non-identifier library name)
 # https://github.com/leanprover/lean4/issues/2865
 
 echo "# TEST: Non-identifier library names"
 test_run new 123-hello
-test_run -d 123-hello exe 123-hello
+test_std 123-hello 123Hello
 
 # Test creating packages with components that contain `.`s
 # https://github.com/leanprover/lean4/issues/2999
@@ -140,23 +156,23 @@ test_run -d 123-hello exe 123-hello
 if [ "$OSTYPE" != "cygwin" -a "$OSTYPE" != "msys" ]; then
   echo "# TEST: Escaped names"
   test_run new «A.B».«C.D»
-  test_run -d A-B-C-D exe a-b-c-d
+  test_std A-B-C-D A.B/C.D a-b-c-d
 fi
 
 # Test creating packages with keyword names
 # https://github.com/leanprover/lake/issues/128
 
 echo "# TEST: Keyword names"
 test_run new meta
-test_run -d meta exe meta
+test_std meta Meta
 
 # Test `init` with name
 
 echo "# TEST: init <name>"
 mkdir hello_world
 pushd hello_world
 test_run init hello_world exe
-test_run exe hello_world
+test_exe . HelloWorld hello_world
 popd
 
 # Test bare `init` on existing package (should error)