feat: lake: avoid use of Lean root directories (#8981)

This PR removes Lake's usage of `lean -R` and `moduleNameOfFileName` to
pass module names to Lean. For workspace names, it now relies on
directly passing the module name through `lean --setup`. For
non-workspace modules passed to `lake lean` or `lake setup-file`, it
uses a fixed module name of `_unknown`.

This means that `lake lean` and `lake setup-file` can be successfully
and consistently used on modules that do not lie under the working
directory or the workspace root.

src/lake/Lake/Build/Actions.lean

@@ -27,11 +27,9 @@ def compileLeanModule
   (arts : ModuleArtifacts)
   (leanArgs : Array String := #[])
   (leanPath : SearchPath := [])
-  (rootDir : FilePath := ".")
   (lean : FilePath := "lean")
 : LogIO Unit := do
-  let mut args := leanArgs ++
-    #[leanFile.toString, "-R", rootDir.toString]
+  let mut args := leanArgs.push leanFile.toString
   if let some oleanFile := arts.olean? then
     createParentDirs oleanFile
     args := args ++ #["-o", oleanFile.toString]

src/lake/Lake/Build/Module.lean

@@ -336,7 +336,7 @@ def Module.recBuildLean (mod : Module) : FetchM (Job ModuleArtifacts) := do
       let args := mod.weakLeanArgs ++ mod.leanArgs
       let relSrcFile := relPathFrom mod.pkg.dir srcFile
       compileLeanModule srcFile relSrcFile setup mod.setupFile arts args
-        (← getLeanPath) mod.rootDir (← getLean)
+        (← getLeanPath) (← getLean)
       mod.clearOutputHashes
     unless upToDate && (← getTrustHash) do
       mod.cacheOutputHashes

src/lake/Lake/CLI/Main.lean

@@ -546,11 +546,11 @@ private def evalLeanFile
     if let some mod := ws.findModuleBySrc? path then
       let setup ← ws.runBuild (cfg := buildConfig) do
         withRegisterJob s!"{mod.name}:setup" do mod.setup.fetch
-      mkArgs path setup (some mod.rootDir) mod.leanArgs
+      mkArgs path setup mod.leanArgs
     else
       let header ← Lean.parseImports' (← IO.FS.readFile path) leanFile.toString
       let setup ← mkModuleSetup ws leanFile.toString header ws.leanOptions buildConfig
-      mkArgs path setup none ws.root.moreLeanArgs
+      mkArgs path setup ws.root.moreLeanArgs
   let spawnArgs : IO.Process.SpawnArgs := {
     args := args ++ moreArgs
     cmd := ws.lakeEnv.lean.lean.toString
@@ -560,15 +560,13 @@ private def evalLeanFile
   let child ← IO.Process.spawn spawnArgs
   child.wait
 where
-  mkArgs leanFile setup rootDir? cfgArgs := do
-    let mut args := cfgArgs.push leanFile.toString
-    if let some rootDir := rootDir? then
-      args := args ++ #["-R", rootDir.toString]
+  mkArgs leanFile setup cfgArgs := do
+    let args := cfgArgs.push leanFile.toString
     let (h, setupFile) ← IO.FS.createTempFile
     let contents := (toJson setup).compress
     logVerbose s!"module setup: {contents}"
     h.putStr contents
-    args := args ++ #["--setup", setupFile.toString]
+    let args := args ++ #["--setup", setupFile.toString]
     return args
 
 protected def lean : CliM PUnit := do

src/lake/Lake/CLI/Serve.lean

@@ -28,7 +28,7 @@ def mkModuleSetup
 : IO ModuleSetup := do
   let {dynlibs, plugins} ← ws.runBuild (buildImportsAndDeps fileName header.imports) buildConfig
   return {
-    name := ← Lean.moduleNameOfFileName fileName none
+    name := `_unknown
     isModule := header.isModule
     imports? := none
     importArts := {} -- TODO

src/lake/tests/init/test.sh

@@ -150,6 +150,11 @@ popd
 echo "# TEST: init existing"
 test_err "package already initialized" -d hello_world init
 
+# Tests of the `math` template are usually disabled as they fail unless Mathlib
+# and Lean are synchronized. However, it remains here as it useful when testing
+# changes to the template.
+if false; then
+
 # Test that Mathlib-standard packages have the expected strict linter options.
 mkdir mathlib_standards
 pushd mathlib_standards
@@ -171,5 +176,7 @@ echo >>MathlibStandards.lean "#guard true"
 test_cmd_out 'note: this linter can be disabled with `set_option linter.hashCommand false`' $ELAN run $(cat lean-toolchain) lake build mathlib_standards
 popd
 
+fi
+
 # Cleanup
 rm -f produced.out

src/lake/tests/lean/test.sh

@@ -14,5 +14,8 @@ test_out 'Hello Bob!' lean Test.lean -- --run Test.lean Bob
 # if the source file is a module in the workspace
 test_out '"options":{"weak.foo":"bar"}' -v lean Lib/Basic.lean
 
+# Test running a file works outside the workspace and working directory
+test_out '"name":"_unknown"' -v lean ../../examples/hello/Hello.lean
+
 # cleanup
 rm -f produced.out

src/lake/tests/setupFile/test.sh

@@ -7,6 +7,9 @@ source ../common.sh
 # Test `setup-file` functionality
 #---
 
+# 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, by default, no plugins are used.
 test_out '"plugins":[]' setup-file ImportFoo.lean