fix: do not strip dotted components from lean module names (#2994)

This introduces `FilePath.addExtension` to take a path that we know has
no prior extension, and append a new extension to it.
As this function is simpler than `FilePath.withExtension`, this change
eagerly replaces uses of the latter with the former, except in a few
cases where stripping the extension really is the right thing to do.

This should fix the bug described at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Import.20file.20with.20multiple.20dots.20in.20file.20name/near/404508048,
where `import «A.B».«C.D.lean»` is needed to import `A.B/C.D.lean`.

Closes #2999

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

src/Init/System/FilePath.lean

@@ -101,6 +101,21 @@ def withFileName (p : FilePath) (fname : String) : FilePath :=
   | none => ⟨fname⟩
   | some p => p / fname
 
+/-- Appends the extension `ext` to a path `p`.
+
+`ext` should not contain a leading `.`, as this function adds one.
+If `ext` is the empty string, no `.` is added.
+
+Unlike `System.FilePath.withExtension`, this does not remove any existing extension. -/
+def addExtension (p : FilePath) (ext : String) : FilePath :=
+  match p.fileName with
+  | none => p
+  | some fname => p.withFileName (if ext.isEmpty then fname else fname ++ "." ++ ext)
+
+/-- Replace the current extension in a path `p` with `ext`.
+
+`ext` should not contain a `.`, as this function adds one.
+If `ext` is the empty string, no `.` is added. -/
 def withExtension (p : FilePath) (ext : String) : FilePath :=
   match p.fileStem with
   | none => p

src/Lean/Server/Watchdog.lean

@@ -677,7 +677,7 @@ def initAndRunWatchdogAux : ServerM Unit := do
 def findWorkerPath : IO System.FilePath := do
   let mut workerPath ← IO.appPath
   if let some path := (←IO.getEnv "LEAN_SYSROOT") then
-    workerPath := System.FilePath.mk path / "bin" / "lean" |>.withExtension System.FilePath.exeExtension
+    workerPath := System.FilePath.mk path / "bin" / "lean" |>.addExtension System.FilePath.exeExtension
   if let some path := (←IO.getEnv "LEAN_WORKER_PATH") then
     workerPath := System.FilePath.mk path
   return workerPath

src/Lean/Util/Path.lean

@@ -28,7 +28,7 @@ def realPathNormalized (p : FilePath) : IO FilePath :=
   return (← IO.FS.realPath p).normalize
 
 def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
-  go mod |>.withExtension ext
+  go mod |>.addExtension ext
 where
   go : Name → FilePath
   | Name.str p h => go p / h
@@ -46,7 +46,7 @@ not check whether the returned path exists. -/
 def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
   let pkg := mod.getRoot.toString (escape := false)
   let root? ← sp.findM? fun p =>
-    (p / pkg).isDir <||> ((p / pkg).withExtension ext).pathExists
+    (p / pkg).isDir <||> ((p / pkg).addExtension ext).pathExists
   return root?.map (modToFilePath · mod ext)
 
 /-- Like `findWithExt`, but ensures the returned path exists. -/

src/lake/Lake/CLI/Init.lean

@@ -218,16 +218,17 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.En
 
 def validatePkgName (pkgName : String) : LogIO PUnit := do
   if pkgName.isEmpty || pkgName.all (· == '.') || pkgName.any (· ∈ ['/', '\\']) then
-    error "illegal package name"
+    error s!"illegal package name '{pkgName}'"
   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
+      let path ← IO.FS.realPath cwd
+      match path.fileName with
       | some dirName => pure dirName
-      | none => error "illegal package name"
+      | none => error s!"illegal package name: could not derive one from '{path}'"
     else
       pure pkgName
   let pkgName := pkgName.trim

src/lake/Lake/Config/InstallPath.lean

@@ -12,7 +12,7 @@ namespace Lake
 
 /-- Standard path of `elan` in a Elan installation. -/
 def elanExe (home : FilePath) :=
-  home / "bin" / "elan" |>.withExtension FilePath.exeExtension
+  home / "bin" / "elan" |>.addExtension FilePath.exeExtension
 
 /-- Information about the local Elan setup. -/
 structure ElanInstall where
@@ -24,19 +24,19 @@ structure ElanInstall where
 
 /-- Standard path of `lean` in a Lean installation. -/
 def leanExe (sysroot : FilePath) :=
-  sysroot / "bin" / "lean" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "lean" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `leanc` in a Lean installation. -/
 def leancExe (sysroot : FilePath) :=
-  sysroot / "bin" / "leanc" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "leanc" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `llvm-ar` in a Lean installation. -/
 def leanArExe (sysroot : FilePath) :=
-  sysroot / "bin" / "llvm-ar" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "llvm-ar" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `clang` in a Lean installation. -/
 def leanCcExe (sysroot : FilePath) :=
-  sysroot / "bin" / "clang" |>.withExtension FilePath.exeExtension
+  sysroot / "bin" / "clang" |>.addExtension FilePath.exeExtension
 
 /-- Standard path of `libleanshared` in a Lean installation. -/
 def leanSharedLib (sysroot : FilePath) :=
@@ -45,7 +45,7 @@ def leanSharedLib (sysroot : FilePath) :=
       sysroot / "bin"
     else
       sysroot / "lib" / "lean"
-  dir / "libleanshared" |>.withExtension sharedLibExt
+  dir / "libleanshared" |>.addExtension sharedLibExt
 
 /-- Path information about the local Lean installation. -/
 structure LeanInstall where
@@ -80,7 +80,7 @@ def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
 
 /-- Standard path of `lake` in a Lake installation. -/
 def lakeExe (buildHome : FilePath) :=
-  buildHome / "bin" / "lake" |>.withExtension FilePath.exeExtension
+  buildHome / "bin" / "lake" |>.addExtension FilePath.exeExtension
 
 /-- Path information about the local Lake installation. -/
 structure LakeInstall where
@@ -203,7 +203,7 @@ try to return their joint home by assuming they are both located at `<home>/bin`
 def findLakeLeanJointHome? : BaseIO (Option FilePath) := do
   if let .ok appPath ← IO.appPath.toBaseIO then
     if let some appDir := appPath.parent then
-      let leanExe := appDir / "lean" |>.withExtension FilePath.exeExtension
+      let leanExe := appDir / "lean" |>.addExtension FilePath.exeExtension
       if (← leanExe.pathExists) then
         return appDir.parent
   return none

src/lake/Lake/Config/LeanExe.lean

@@ -61,7 +61,7 @@ The file name of binary executable
 (i.e., `exeName` plus the platform's `exeExtension`).
 -/
 @[inline] def fileName (self : LeanExe) : FilePath :=
-  FilePath.withExtension self.config.exeName FilePath.exeExtension
+  FilePath.addExtension self.config.exeName FilePath.exeExtension
 
 /-- The path to the executable in the package's `binDir`. -/
 @[inline] def file (self : LeanExe) : FilePath :=

src/lake/tests/init/.gitignore

@@ -5,5 +5,6 @@
 /hello-exe
 /lean-data
 /123-hello
+/«A.B».«C.D»
 /meta
 /qed

src/lake/tests/init/clean.sh

@@ -5,5 +5,6 @@ rm -rf hello_world
 rm -rf hello-exe
 rm -rf lean-data
 rm -rf 123-hello
+rm -rf «A-B»-«C-D»
 rm -rf meta
 rm -rf qed

src/lake/tests/init/test.sh

@@ -77,6 +77,15 @@ $LAKE -d lean-data exe lean-data
 $LAKE new 123-hello
 $LAKE -d 123-hello exe 123-hello
 
+# Test creating packages with components that contain `.`s
+# https://github.com/leanprover/lean4/issues/2999
+  
+# this fails on windows for unrelated reasons
+if [ "$OSTYPE" != "msys" ]; then
+  $LAKE new «A.B».«C.D»
+  $LAKE -d «A-B»-«C-D» exe «a.b-c.d»
+fi
+
 # Test creating packages with keyword names
 # https://github.com/leanprover/lake/issues/128
 

tests/lean/filePath.lean

@@ -30,3 +30,5 @@ def norm (f : FilePath) : String :=
 #eval norm <| FilePath.withExtension "a/b.tar.gz" "xz"
 #eval norm <| FilePath.withExtension "a/b.tar.gz" ""
 #eval norm <| FilePath.withExtension "a/b" "tar.gz"
+
+#eval norm <| FilePath.addExtension "a/b.tar.gz" "bak"

tests/lean/filePath.lean.expected.out

@@ -17,3 +17,4 @@ none
 "a/b.tar.xz"
 "a/b.tar"
 "a/b.tar.gz"
+"a/b.tar.gz.bak"