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

@@ -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 :=

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

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

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