From 311ae6168d4da8548bdd32c827295fabf0db60b4 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 24 Jun 2025 21:04:13 -0400 Subject: [PATCH] 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 | 4 +--- src/lake/Lake/Build/Module.lean | 2 +- src/lake/Lake/CLI/Main.lean | 12 +++++------- src/lake/Lake/CLI/Serve.lean | 2 +- src/lake/tests/init/test.sh | 7 +++++++ src/lake/tests/lean/test.sh | 3 +++ src/lake/tests/setupFile/test.sh | 3 +++ 7 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index 8d8af5e3a5..966c12e94a 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/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] diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index d97864a6b6..a8d104e286 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 431711bf2a..1b4e2e1e02 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 10af416fb4..94d2738cad 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/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 diff --git a/src/lake/tests/init/test.sh b/src/lake/tests/init/test.sh index 414d8d91cc..680e0e4882 100755 --- a/src/lake/tests/init/test.sh +++ b/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 diff --git a/src/lake/tests/lean/test.sh b/src/lake/tests/lean/test.sh index 06dcfa0469..59954ef552 100755 --- a/src/lake/tests/lean/test.sh +++ b/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 diff --git a/src/lake/tests/setupFile/test.sh b/src/lake/tests/setupFile/test.sh index 963ff3cc96..93d671369c 100755 --- a/src/lake/tests/setupFile/test.sh +++ b/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