chore: update Lean to 06-01

also:
* refactor code relying on the old `toName`
* do not decapitalize package names in `lake new`

Lake/CLI/Build.lean

@@ -43,7 +43,7 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
   if spec.isEmpty then
     return ws.root
   else
-    match ws.findPackage? spec.toName with
+    match ws.findPackage? <| stringToLegalOrSimpleName spec with
     | some pkg => return pkg
     | none => throw <| CliError.unknownPackage spec
 
@@ -150,7 +150,7 @@ def resolveTargetBaseSpec
       else
         throw <| CliError.unknownModule mod
     else
-      resolveTargetInWorkspace ws spec.toName facet
+      resolveTargetInWorkspace ws (stringToLegalOrSimpleName spec) facet
   | [pkgSpec, targetSpec] =>
     let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec
     let pkg ← parsePackageSpec ws pkgSpec

Lake/CLI/Init.lean

@@ -139,18 +139,18 @@ where
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
 def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit := do
-  let pkgName := name.decapitalize.toName
+  let pkgName := stringToLegalOrSimpleName name
 
   -- determine the name to use for the root
   -- use upper camel case unless the specific module name already exists
   let (root, rootFile, rootExists) ← do
-    let root := name.toName
+    let root := pkgName
     let rootFile := Lean.modToFilePath dir root "lean"
     let rootExists ← rootFile.pathExists
     if tmp = .exe || rootExists then
       pure (root, rootFile, rootExists)
     else
-      let root := toUpperCamelCase root
+      let root := toUpperCamelCase (toUpperCamelCaseString name |>.toName)
       let rootFile := Lean.modToFilePath dir root "lean"
       pure (root, rootFile, ← rootFile.pathExists)
 

Lake/Config/Glob.lean

@@ -27,10 +27,10 @@ partial def forEachModuleIn [Monad m] [MonadLiftT IO m]
 (dir : FilePath) (f : Name → m PUnit) : m PUnit := do
   for entry in (← dir.readDir) do
     if (← liftM (m := IO) <| entry.path.isDir) then
-      let n := entry.fileName.toName
+      let n := Name.mkSimple entry.fileName
       f n *> forEachModuleIn entry.path (f <| n ++ ·)
     else if entry.path.extension == some "lean" then
-      f <| FilePath.withExtension entry.fileName "" |>.toString.toName
+      f <| Name.mkSimple <| FilePath.withExtension entry.fileName "" |>.toString
 
 namespace Glob
 

Lake/Config/Package.lean

@@ -39,6 +39,14 @@ def nameToArchive (name? : Option String) : String :=
   | none => archiveSuffix
   | some name => s!"{name}-{archiveSuffix}"
 
+/--
+First tries to convert a string into a legal name.
+If that fails, defaults to making it a simple name (e.g., `Lean.Name.mkSimple`).
+Currently used for package and target names taken from the CLI.
+-/
+def stringToLegalOrSimpleName (s : String) : Name :=
+  if s.toName.isAnonymous then Lean.Name.mkSimple s else s.toName
+
 --------------------------------------------------------------------------------
 /-! # Defaults -/
 --------------------------------------------------------------------------------

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-04-04
+leanprover/lean4:nightly-2023-06-01