diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index 6091a0a152..af1c8eba54 100644 --- a/src/Lean/Util/Path.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 820da18156..a689f8d55f 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/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) diff --git a/src/lake/tests/init/.gitignore b/src/lake/tests/init/.gitignore index f5af1dcb0c..83917dc4f8 100644 --- a/src/lake/tests/init/.gitignore +++ b/src/lake/tests/init/.gitignore @@ -2,4 +2,5 @@ /hello_world /hello-world /lean-data +/123-hello /meta diff --git a/src/lake/tests/init/clean.sh b/src/lake/tests/init/clean.sh index 8cdf5db3b9..696cba217a 100755 --- a/src/lake/tests/init/clean.sh +++ b/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 diff --git a/src/lake/tests/init/test.sh b/src/lake/tests/init/test.sh index 4251964240..2b693731c5 100755 --- a/src/lake/tests/init/test.sh +++ b/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