fix: lake: proper exe targets & pkg generation (leanprover#2932)

Improves executable handling in `lake exe` and `lake init`:

* `lake exe <target>` now parses `target` like a build target (as the
help text states it should) rather than as a basic name.
* `lake new foo.bar [std]` now generates executables named `foo-bar`.
* `lake new foo.bar exe` now properly creates `foo/bar.lean`.

src/lake/Lake/CLI/Build.lean

@@ -165,7 +165,24 @@ def resolveTargetBaseSpec
       else
         throw <| CliError.unknownModule mod
     else
-      resolveTargetInPackage ws pkg targetSpec facet
+      resolveTargetInPackage ws pkg (stringToLegalOrSimpleName targetSpec) facet
+  | _ =>
+    throw <| CliError.invalidTargetSpec spec '/'
+
+def parseExeTargetSpec (ws : Workspace) (spec : String) : Except CliError LeanExe := do
+  match spec.splitOn "/" with
+  | [targetSpec] =>
+    let targetName := stringToLegalOrSimpleName targetSpec
+    match ws.findLeanExe? targetName with
+    | some exe => return exe
+    | none => throw <| CliError.unknownExe spec
+  | [pkgSpec, targetSpec] =>
+    let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec
+    let pkg ← parsePackageSpec ws pkgSpec
+    let targetName := stringToLegalOrSimpleName targetSpec
+    match pkg.findLeanExe? targetName with
+    | some exe => return exe
+    | none => throw <| CliError.unknownExe spec
   | _ =>
     throw <| CliError.invalidTargetSpec spec '/'
 

src/lake/Lake/CLI/Error.lean

@@ -29,6 +29,8 @@ inductive CliError
 | nonCliFacet (type : String) (facet : Name)
 | invalidTargetSpec (spec : String) (tooMany : Char)
 | invalidFacet (target : Name) (facet : Name)
+/- Executable CLI Errors -/
+| unknownExe (spec : String)
 /- Script CLI Error -/
 | unknownScript (script : String)
 | missingScriptDoc (script : String)
@@ -61,6 +63,7 @@ def toString : CliError → String
 | nonCliFacet t f         => s!"{t} facet `{f.toString false}` is not a buildable via `lake`"
 | invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
 | invalidFacet t f        => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets"
+| unknownExe s            => s!"unknown executable {s}"
 | unknownScript s         => s!"unknown script {s}"
 | missingScriptDoc s      => s!"no documentation provided for `{s}`"
 | invalidScriptSpec s     => s!"invalid script spec '{s}' (too many '/')"

src/lake/Lake/CLI/Init.lean

@@ -138,19 +138,21 @@ def InitTemplate.parse? : String → Option InitTemplate
 | "math" => some .math
 | _ => none
 
-def InitTemplate.configFileContents (pkgName root : String) : InitTemplate → String
-| .std => stdConfigFileContents pkgName root pkgName.toLower
-| .lib => libConfigFileContents pkgName root
-| .exe => exeConfigFileContents pkgName root
-| .math => mathConfigFileContents pkgName root
+def escapeIdent (id : String) : String :=
+  Lean.idBeginEscape.toString ++ id ++ Lean.idEndEscape.toString
 
 def escapeName! : Name → String
-| .anonymous        => "[anonymous]"
-| .str .anonymous s => escape s
-| .str n s          => escapeName! n ++ "." ++ escape s
+| .anonymous        => unreachable!
+| .str .anonymous s => escapeIdent s
+| .str n s          => escapeName! n ++ "." ++ escapeIdent s
 | _                 => unreachable!
-where
-  escape s :=  Lean.idBeginEscape.toString ++ s ++ Lean.idEndEscape.toString
+
+def InitTemplate.configFileContents (pkgName : Name) (root : String) : InitTemplate → String
+| .std => stdConfigFileContents (escapeName! pkgName) root
+  (escapeIdent <| pkgName.toStringWithSep "-" false).toLower
+| .lib => libConfigFileContents (escapeName! pkgName) root
+| .exe => exeConfigFileContents (escapeName! pkgName) root
+| .math => mathConfigFileContents (escapeName! pkgName) root
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
 def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit := do
@@ -174,12 +176,13 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En
   if (← configFile.pathExists) then
     error  "package already initialized"
   let rootNameStr := escapeName! root
-  let contents := tmp.configFileContents (escapeName! pkgName) rootNameStr
+  let contents := tmp.configFileContents pkgName rootNameStr
   IO.FS.writeFile configFile contents
 
   -- write example code if the files do not already exist
   if tmp = .exe then
     unless (← rootFile.pathExists) do
+      createParentDirs rootFile
       IO.FS.writeFile rootFile exeFileContents
   else
     unless rootExists do

src/lake/Lake/CLI/Main.lean

@@ -366,14 +366,14 @@ protected def env : CliM PUnit := do
     exit 0
 
 protected def exe : CliM PUnit := do
-  let exeName ← takeArg "executable name"
+  let exeSpec ← takeArg "executable target"
   let args ← takeArgs
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let ws ← loadWorkspace config
-  let ctx := mkLakeContext ws
-  let buildConfig := mkBuildConfig opts
-  exit <| ← (exe exeName args.toArray buildConfig).run ctx
+  let exe ← parseExeTargetSpec ws exeSpec
+  let exeFile ← ws.runBuild (exe.build >>= (·.await)) <| mkBuildConfig opts
+  exit <| ← (env exeFile.toString args.toArray).run <| mkLakeContext ws
 
 protected def selfCheck : CliM PUnit := do
   processOptions lakeOption

src/lake/examples/targets/test.sh

@@ -1,6 +1,9 @@
 #!/usr/bin/env bash
 set -exo pipefail
 
+# Prevent MSYS2 from automatically transforming path-like targets
+[ "$OSTYPE" == "msys" ] && export MSYS2_ARG_CONV_EXCL=*
+
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 if [ "$OS" = Windows_NT ]; then
@@ -75,6 +78,10 @@ cat ./.lake/build/caw.txt | grep Caw!
 $LAKE build a b
 ./.lake/build/bin/a
 ./.lake/build/bin/b
+$LAKE exe @targets/a
+$LAKE exe targets/a
+$LAKE exe /b
+$LAKE exe b
 
 # Test repeat build works
 $LAKE build bark | grep Bark!

src/lake/tests/init/.gitignore

@@ -2,6 +2,7 @@
 /HelloWorld
 /hello_world
 /hello-world
+/hello-exe
 /lean-data
 /123-hello
 /meta

src/lake/tests/init/clean.sh

@@ -2,6 +2,7 @@ rm -rf hello
 rm -rf HelloWorld
 rm -rf hello-world
 rm -rf hello_world
+rm -rf hello-exe
 rm -rf lean-data
 rm -rf 123-hello
 rm -rf meta

src/lake/tests/init/test.sh

@@ -14,68 +14,67 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Test package name validation (should error)
 # https://github.com/leanprover/lean4/issues/2637
 
-($LAKE new '  ' 2>&1 && false || true) | grep "illegal package name"
-($LAKE new .    2>&1 && false || true) | grep "illegal package name"
-($LAKE new ..   2>&1 && false || true) | grep "illegal package name"
-($LAKE new .... 2>&1 && false || true) | grep "illegal package name"
-($LAKE new a/bc 2>&1 && false || true) | grep "illegal package name"
-($LAKE new a\\b 2>&1 && false || true) | grep "illegal package name"
-($LAKE new init 2>&1 && false || true) | grep "reserved package name"
-($LAKE new Lean 2>&1 && false || true) | grep "reserved package name"
-($LAKE new Lake 2>&1 && false || true) | grep "reserved package name"
-($LAKE new main 2>&1 && false || true) | grep "reserved package name"
+($LAKE new  .    2>&1 && false || true) | grep "illegal package name"
+for cmd in new init; do
+($LAKE $cmd ..   2>&1 && false || true) | grep "illegal package name"
+($LAKE $cmd .... 2>&1 && false || true) | grep "illegal package name"
+($LAKE $cmd '  ' 2>&1 && false || true) | grep "illegal package name"
+($LAKE $cmd a/bc 2>&1 && false || true) | grep "illegal package name"
+($LAKE $cmd a\\b 2>&1 && false || true) | grep "illegal package name"
+($LAKE $cmd init 2>&1 && false || true) | grep "reserved package name"
+($LAKE $cmd Lean 2>&1 && false || true) | grep "reserved package name"
+($LAKE $cmd Lake 2>&1 && false || true) | grep "reserved package name"
+($LAKE $cmd main 2>&1 && false || true) | grep "reserved package name"
+done
 
 # Test `init .`
 
 mkdir hello
 pushd hello
 $LAKE1 init .
-$LAKE1 build
-.lake/build/bin/hello
+$LAKE1 exe hello
 popd
 
 # Test creating packages with uppercase names
 # https://github.com/leanprover/lean4/issues/2540
 
 $LAKE new HelloWorld
-$LAKE -d HelloWorld build
-HelloWorld/.lake/build/bin/helloworld
+$LAKE -d HelloWorld exe helloworld
 
 # Test creating multi-level packages with a `.`
 
 $LAKE new hello.world
-$LAKE -d hello-world build
-hello-world/.lake/build/bin/hello-world
+$LAKE -d hello-world exe hello-world
 test -f hello-world/Hello/World/Basic.lean
 
+$LAKE new hello.exe exe
+$LAKE -d hello-exe exe hello.exe
+test -f hello-exe/hello/exe.lean
+
 # 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
 
 $LAKE new lean-data
-$LAKE -d lean-data build
-lean-data/.lake/build/bin/lean-data
+$LAKE -d lean-data exe lean-data
 
 # Test creating packages starting with digits (i.e., a non-identifier library name)
 # https://github.com/leanprover/lean4/issues/2865
 
 $LAKE new 123-hello
-$LAKE -d 123-hello build
-123-hello/.lake/build/bin/123-hello
+$LAKE -d 123-hello exe 123-hello
 
 # Test creating packages with keyword names
 # https://github.com/leanprover/lake/issues/128
 
 $LAKE new meta
-$LAKE -d meta build
-meta/.lake/build/bin/meta
+$LAKE -d meta exe meta
 
 # Test `init` with name
 
 mkdir hello_world
 pushd hello_world
 $LAKE1 init hello_world exe
-$LAKE1 build
-./.lake/build/bin/hello_world
+$LAKE1 exe hello_world
 popd
 
 # Test bare `init` on existing package (should error)