From 52855ce1c186212322a2c94cb0813ecaa89dbf2d Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sun, 3 Aug 2025 01:18:59 -0400
Subject: [PATCH] fix: lake: module lookup by source w/ multiple `.` (#9697)

This PR fixes the handling in `lake lean` and `lake setup-file` of a
library source file with multiple dots (e.g., `src/Foo.Bar.lean`).
---
 src/lake/Lake/Config/Module.lean           | 11 +++++++++--
 src/lake/Lake/Util/FilePath.lean           |  2 ++
 src/lake/tests/lean/Lib/Foo.Bar.lean       |  0
 src/lake/tests/lean/test.sh                |  3 +++
 src/lake/tests/setupFile/Test/Foo.Bar.lean |  0
 src/lake/tests/setupFile/test.sh           |  4 ++++
 6 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 src/lake/tests/lean/Lib/Foo.Bar.lean
 create mode 100644 src/lake/tests/setupFile/Test/Foo.Bar.lean

diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean
index 1d3192fd9f..09abe97b78 100644
--- a/src/lake/Lake/Config/Module.lean
+++ b/src/lake/Lake/Config/Module.lean
@@ -44,11 +44,18 @@ Locate the named, buildable module in the library
 def LeanLib.findModule? (mod : Name) (self : LeanLib) : Option Module :=
   if self.isBuildableModule mod then some {lib := self, name := mod} else none
 
-/-- Returns the buildable module in the library whose source file is `path`.  -/
+/--
+Returns the buildable module in the library whose source file or directory is `path`.
+
+For example, in a library with a source directory of `src`,
+`src/Foo/Bar.lean` and `src/Foo/Bar/` will both resolve to the module `Foo.Bar`.
+-/
 def LeanLib.findModuleBySrc? (path : FilePath) (self : LeanLib) : Option Module := do
   let modPath ← path.toString.dropPrefix? self.srcDir.toString
   let modPath := (modPath.drop 1).toString -- remove leading `/`
-  self.findModule? (modOfFilePath modPath)
+  let modPath ← modPath.dropSuffix? ".lean" <|> modPath.dropSuffix? FilePath.pathSeparator.toString
+  let modName := FilePath.components modPath.toString |>.foldl .str .anonymous
+  self.findModule? modName
 
 /-- Locate the named, buildable, importable, local module in the package.  -/
 def Package.findModule? (mod : Name) (self : Package) : Option Module :=
diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean
index 5feb5348d3..85b3cfb6ec 100644
--- a/src/lake/Lake/Util/FilePath.lean
+++ b/src/lake/Lake/Util/FilePath.lean
@@ -86,3 +86,5 @@ example :
   ∧ modOfFilePath "Foo/Bar.tar.gz" = `Foo.Bar
   ∧ modOfFilePath "Foo/Bar.lean/" = `Foo.«Bar.lean»
 := by native_decide
+
+attribute [deprecated "Deprecated without replacement." (since := "2025-08-01")] modOfFilePath
diff --git a/src/lake/tests/lean/Lib/Foo.Bar.lean b/src/lake/tests/lean/Lib/Foo.Bar.lean
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/lake/tests/lean/test.sh b/src/lake/tests/lean/test.sh
index 64e46cb8d7..92a60bc78e 100755
--- a/src/lake/tests/lean/test.sh
+++ b/src/lake/tests/lean/test.sh
@@ -22,5 +22,8 @@ test_out '"importArts":{"Lib.Basic":["' -v lean Test.lean
 # Test running a file works outside the workspace and working directory
 test_out '"name":"_unknown"' -v lean ../../examples/hello/Hello.lean
 
+# Test running a library file with a `.` in its name works
+test_out '"name":"Lib.«Foo.Bar»"' -v lean Lib/Foo.Bar.lean
+
 # cleanup
 rm -f produced.out
diff --git a/src/lake/tests/setupFile/Test/Foo.Bar.lean b/src/lake/tests/setupFile/Test/Foo.Bar.lean
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/lake/tests/setupFile/test.sh b/src/lake/tests/setupFile/test.sh
index 7e56f8fc03..b8c1d19ff4 100755
--- a/src/lake/tests/setupFile/test.sh
+++ b/src/lake/tests/setupFile/test.sh
@@ -10,6 +10,10 @@ source ../common.sh
 # Test that setup-file works on a file outside the workspace and working directory
 test_out '"name":"_unknown"' setup-file ../../examples/hello/Hello.lean
 
+# Test that setup-file works on library files with a `.` in their name
+# https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Foo.2E.2Elean.20works.20when.20.60import.60ed.20but.20not.20in.20vscode/near/529702293
+test_out '"name":"Test.«Foo.Bar»"' setup-file Test/Foo.Bar.lean
+
 # Test that, by default, no plugins are used.
 test_out '"plugins":[]' setup-file ImportFoo.lean