From cf216ecd16e412c1b1eef1ce11c71305475eea94 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 8 Jun 2023 02:06:13 -0400
Subject: [PATCH] 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      | 4 ++--
 Lake/CLI/Init.lean       | 6 +++---
 Lake/Config/Glob.lean    | 4 ++--
 Lake/Config/Package.lean | 8 ++++++++
 lean-toolchain           | 2 +-
 5 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index c7d581db16..0929c1b432 100644
--- a/Lake/CLI/Build.lean
+++ b/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
diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean
index b32ebbcffb..037f04d249 100644
--- a/Lake/CLI/Init.lean
+++ b/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)
 
diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean
index fb920434a2..da35fe0b6f 100644
--- a/Lake/Config/Glob.lean
+++ b/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
 
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 980092f779..d6cb45cea5 100644
--- a/Lake/Config/Package.lean
+++ b/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 -/
 --------------------------------------------------------------------------------
diff --git a/lean-toolchain b/lean-toolchain
index aa048911b3..5278e43a75 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-04-04
+leanprover/lean4:nightly-2023-06-01