feat: bare lake init & validated pkg names

src/lake/Lake/CLI/Help.lean

@@ -63,9 +63,12 @@ def helpInit :=
 s!"Create a Lean package in the current directory
 
 USAGE:
-  lake init <name> [<template>]
+  lake init [<name>] [<template>]
 
-{templateHelp}"
+{templateHelp}
+
+You can create a package with current directory's name via `lake init .`
+or a bare `lake init`."
 
 def helpBuild :=
 "Build targets

src/lake/Lake/CLI/Init.lean

@@ -233,10 +233,28 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En
     else
       logWarning "failed to initialize git repository"
 
-def init (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit :=
-  initPkg "." pkgName tmp env
-
-def new (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit := do
-  let dirName := pkgName.map fun chr => if chr == '.' then '-' else chr
-  IO.FS.createDir dirName
+def validatePkgName (pkgName : String) : LogIO PUnit := do
+  if pkgName.isEmpty || pkgName.all (· == '.') || pkgName.any (· ∈ ['/', '\\']) then
+    error "illegal package name"
+  if pkgName.toLower ∈ ["init", "lean", "lake", "main"] then
+    error "reserved package name"
+
+def init (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do
+  let pkgName ← do
+    if pkgName == "." then
+      match (← IO.FS.realPath cwd).fileName with
+      | some dirName => pure dirName
+      | none => error "illegal package name"
+    else
+      pure pkgName
+  let pkgName := pkgName.trim
+  validatePkgName pkgName
+  IO.FS.createDirAll cwd
+  initPkg cwd pkgName tmp env
+
+def new (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do
+  let pkgName := pkgName.trim
+  validatePkgName pkgName
+  let dirName := cwd / pkgName.map fun chr => if chr == '.' then '-' else chr
+  IO.FS.createDirAll dirName
   initPkg dirName pkgName tmp env

src/lake/Lake/CLI/Main.lean

@@ -268,14 +268,14 @@ protected def new : CliM PUnit := do
   let opts ← getThe LakeOptions
   let name ← takeArg "package name"
   let tmp ← parseTemplateSpec <| (← takeArg?).getD ""
-  noArgsRem do MainM.runLogIO (new name tmp (← opts.computeEnv)) opts.verbosity
+  noArgsRem do MainM.runLogIO (new name tmp (← opts.computeEnv) opts.rootDir) opts.verbosity
 
 protected def init : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
-  let name ← takeArg "package name"
+  let name := (← takeArg?).getD "."
   let tmp ← parseTemplateSpec <| (← takeArg?).getD ""
-  noArgsRem do MainM.runLogIO (init name tmp (← opts.computeEnv)) opts.verbosity
+  noArgsRem do MainM.runLogIO (init name tmp (← opts.computeEnv) opts.rootDir) opts.verbosity
 
 protected def build : CliM PUnit := do
   processOptions lakeOption

src/lake/tests/init/.gitignore

@@ -1,4 +1,5 @@
-/Hello
+/hello
+/HelloWorld
 /hello_world
 /hello-world
 /lean-data

src/lake/tests/init/clean.sh

@@ -1,4 +1,5 @@
-rm -rf Hello
+rm -rf hello
+rm -rf HelloWorld
 rm -rf hello-world
 rm -rf hello_world
 rm -rf lean-data

src/lake/tests/init/test.sh

@@ -1,4 +1,5 @@
-set -ex
+#!/usr/bin/env bash
+set -euxo pipefail
 
 ./clean.sh
 
@@ -7,15 +8,38 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 # Test `new` and `init` with bad template (should error)
 
-! $LAKE new foo bar
-! $LAKE init foo bar
+($LAKE new  foo bar 2>&1 && false || true) | grep "unknown package template"
+($LAKE init foo bar 2>&1 && false || true) | grep "unknown package template"
+
+# 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"
+
+# Test `init .`
+
+mkdir hello
+pushd hello
+$LAKE1 init .
+$LAKE1 build
+.lake/build/bin/hello
+popd
 
 # Test creating packages with uppercase names
 # https://github.com/leanprover/lean4/issues/2540
 
-$LAKE new Hello
-$LAKE -d Hello build
-Hello/.lake/build/bin/hello
+$LAKE new HelloWorld
+$LAKE -d HelloWorld build
+HelloWorld/.lake/build/bin/helloworld
 
 # Test creating multi-level packages with a `.`
 
@@ -38,15 +62,15 @@ $LAKE new meta
 $LAKE -d meta build
 meta/.lake/build/bin/meta
 
-# Test `init`
+# Test `init` with name
 
 mkdir hello_world
-
-cd hello_world
+pushd hello_world
 $LAKE1 init hello_world exe
 $LAKE1 build
 ./.lake/build/bin/hello_world
+popd
 
-# Test `init` on existing package (should error)
+# Test bare `init` on existing package (should error)
 
-$LAKE1 init hello_world && exit 1 || true
+($LAKE -d hello_world init 2>&1 && false || true) | grep "package already initialized"