fix: support non-identifier library names

Author: tydeu

src/Lean/Util/Path.lean

@@ -33,7 +33,7 @@ namespace SearchPath
 `ext` (`lean` or `olean`) corresponding to `mod`. Otherwise, return `none`. Does
 not check whether the returned path exists. -/
 def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
-  let pkg := mod.getRoot.toString
+  let pkg := mod.getRoot.toString (escape := false)
   let root? ← sp.findM? fun p =>
     (p / pkg).isDir <||> ((p / pkg).withExtension ext).pathExists
   return root?.map (modToFilePath · mod ext)
@@ -94,7 +94,7 @@ partial def findOLean (mod : Name) : IO FilePath := do
   if let some fname ← sp.findWithExt "olean" mod then
     return fname
   else
-    let pkg := FilePath.mk mod.getRoot.toString
+    let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
     let mut msg := s!"unknown package '{pkg}'"
     let rec maybeThisOne dir := do
       if ← (dir / pkg).isDir then

src/lake/Lake/CLI/Init.lean

@@ -169,7 +169,7 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En
     if tmp = .exe || rootExists then
       pure (root, rootFile, rootExists)
     else
-      let root := toUpperCamelCase (toUpperCamelCaseString name |>.toName)
+      let root := toUpperCamelCase pkgName
       let rootFile := Lean.modToFilePath dir root "lean"
       pure (root, rootFile, ← rootFile.pathExists)
 

src/lake/tests/init/.gitignore

@@ -2,4 +2,5 @@
 /hello_world
 /hello-world
 /lean-data
+/123-hello
 /meta

src/lake/tests/init/clean.sh

@@ -2,4 +2,5 @@ rm -rf Hello
 rm -rf hello-world
 rm -rf hello_world
 rm -rf lean-data
+rm -rf 123-hello
 rm -rf meta

src/lake/tests/init/test.sh

@@ -24,13 +24,20 @@ $LAKE -d hello-world build
 hello-world/.lake/build/bin/hello-world
 test -f hello-world/Hello/World/Basic.lean
 
-# Test creating packages with a `-` (i.e., a non-Lean name)
+# 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
 
+# 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
+
 # Test creating packages with keyword names
 # https://github.com/leanprover/lake/issues/128