fix: lake: import-related bugs (#8026)

This PR fixes bugs in #7809 and #7909 that were not caught partially
because the `badImport` test had been disabled.

**Bugs Fixed:**

* Building by path no longer drops top-level logs.
* "bad import" errors are once again printed.
* Transitively imported precompiled modules are once again loaded during
elaboration.

src/lake/Lake/Build/Imports.lean

@@ -33,7 +33,7 @@ def buildImportsAndDeps
     let precompileImports ← (← computePrecompileImportsAux leanFile imports).await
     let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
     let externLibsJob ← fetchExternLibs pkgs
-    let impLibsJob ← fetchImportLibs imports
+    let impLibsJob ← fetchImportLibs precompileImports
     let dynlibsJob ← root.dynlibs.fetchIn root
     let pluginsJob ← root.plugins.fetchIn root
     modJob.bindM fun _ =>

src/lake/Lake/Build/Module.lean

@@ -208,8 +208,15 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
       logError s!"{mod.leanFile}: module imports itself"
     imp.olean.fetch
   let importJob := Job.mixArray importJobs "import oleans"
+  /-
+  Remark: It should be possible to avoid transitive imports here when the module
+  itself is precompiled, but they are currently kept to perserve the "bad import" errors.
+  -/
+  let precompileImports ← if mod.shouldPrecompile then
+    mod.transImports.fetch else mod.precompileImports.fetch
+  let precompileImports ← precompileImports.await
   let impLibsJob ← Job.collectArray (traceCaption := "import dynlibs") <$>
-    mod.fetchImportLibs directImports mod.shouldPrecompile
+    mod.fetchImportLibs precompileImports mod.shouldPrecompile
   let externLibsJob ← Job.collectArray (traceCaption := "package external libraries") <$>
     mod.pkg.externLibs.mapM (·.dynlib.fetch)
   let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg "module dynlibs"

src/lake/Lake/CLI/Main.lean

@@ -539,7 +539,7 @@ private def evalLeanFile
     | error s!"file not found: {leanFile}"
   let spawnArgs ← id do
     if let some mod := ws.findModuleBySrc? path then
-      let deps ← ws.runBuild mod.deps.fetch buildConfig
+      let deps ← ws.runBuild (withRegisterJob s!"setup ({mod.name})" do mod.deps.fetch) buildConfig
       return mkSpawnArgs ws path deps (some mod.rootDir) mod.leanArgs
     else
       let imports ← Lean.parseImports' (← IO.FS.readFile path) leanFile.toString

src/lake/Lake/CLI/Serve.lean

@@ -62,7 +62,7 @@ def setupFile
     let some ws ← loadWorkspace loadConfig |>.toBaseIO buildConfig.outLv buildConfig.ansiMode
       | error "failed to load workspace"
     if let some mod := ws.findModuleBySrc? path then
-      let deps ← ws.runBuild mod.deps.fetch buildConfig
+      let deps ← ws.runBuild (withRegisterJob s!"setup ({mod.name})" do mod.deps.fetch) buildConfig
       let opts := mod.serverOptions.foldl (init := {}) fun opts opt =>
         opts.insert opt.name opt.value
       let info : FileSetupInfo := {

src/lake/tests/badImport/test.sh

@@ -14,13 +14,16 @@ source ../common.sh
 test_err "Building Etc" build Lib.U Etc
 # Test importing a missing module from outside the workspace
 test_err "U.lean:2:0: unknown module prefix 'Bogus'" build +Lib.U
-test_run setup-file . Bogus # Lake ignores the file (the server will error)
+test_err "U.lean:2:0: error: unknown module prefix 'Bogus'" lean ./Lib/U.lean
+test_run setup-file ./Lib/U.lean # Lake ignores the unknown import (the server will error)
 # Test importing onself
 test_err "S.lean: module imports itself" build +Lib.S
-test_err "S.lean: module imports itself" setup-file ./Lib/S.lean Lib.S
+test_err "S.lean: module imports itself" lean ./Lib/S.lean
+test_err "S.lean: module imports itself" setup-file ./Lib/S.lean
 # Test importing a missing module from within the workspace
 test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B
-test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean Lib.Bogus
+test_err "B.lean: bad import 'Lib.Bogus'" lean ./Lib/B.lean
+test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean
 # Test a vanishing import within the workspace (lean4#3551)
 echo "[Test: Vanishing Import]"
 set -x
@@ -29,10 +32,12 @@ $LAKE build +Lib.B
 rm Lib/Bogus.lean
 set +x
 test_err "B.lean: bad import 'Lib.Bogus'" build +Lib.B
-test_err "B.lean: bad import 'Lib.Bogus'" setup-file . Lib.B
+test_err "B.lean: bad import 'Lib.Bogus'" lean ./Lib/B.lean
+test_err "B.lean: bad import 'Lib.Bogus'" setup-file ./Lib/B.lean
 # Test a module which imports a module containing a bad import
 test_err "B1.lean: bad import 'Lib.B'" build +Lib.B1
-test_err "B1.lean: bad import 'Lib.B'" setup-file ./Lib/B1.lean Lib.B
+test_err "B1.lean: bad import 'Lib.B'" lean ./Lib/B1.lean
+test_err "B1.lean: bad import 'Lib.B'" setup-file ./Lib/B1.lean
 # Test an executable with a bad import does not kill the whole build
 test_err "Building Etc" build X Etc
 # Test an executable which imports a missing module from within the workspace

src/lake/tests/common.sh

@@ -72,6 +72,8 @@ test_err() {
       echo "Lake unexpectedly succeeded."
       return 1
     fi
+  else
+    return 1
   fi
 }
 

src/lake/tests/precompileLink/Downstream.lean

@@ -0,0 +1,3 @@
+import Downstream.Import
+
+#eval greetingRef.get

src/lake/tests/precompileLink/Downstream/Import.lean

@@ -0,0 +1 @@
+import Foo

src/lake/tests/precompileLink/Foo/Baz.lean

@@ -1,3 +1,3 @@
 import FooDep
 
-initialize greetingRef : IO.Ref String ← IO.mkRef greeting
+builtin_initialize greetingRef : IO.Ref String ← IO.mkRef greeting

src/lake/tests/precompileLink/Indirect.lean

@@ -0,0 +1 @@
+import Foo

src/lake/tests/precompileLink/lakefile.lean

@@ -12,3 +12,5 @@ lean_lib Foo where
 lean_lib FooDep
 lean_lib FooDepDep
 lean_exe orderTest
+
+lean_lib Downstream

src/lake/tests/precompileLink/test.sh

@@ -7,6 +7,11 @@ source ../common.sh
 # https://github.com/leanprover/lean4/issues/7790
 test_run -v exe orderTest
 
+# Test that transitively importing a precompiled module
+# from a non-precompiled module works
+test_not_out '"pluginPaths":[]' -v setup-file bogus Downstream
+test_run -v build Downstream
+
 # Test that `moreLinkArgs` are included when linking precompiled modules
 ./clean.sh
 test_maybe_err "-lBogus" build -KlinkArgs=-lBogus

src/shell/CMakeLists.txt

@@ -185,12 +185,11 @@ ENDFOREACH(T)
 # bootstrap: too slow
 # toolchain: requires elan to download toolchain
 # online: downloads remote repositories
-# badImport/buildArgs: flaky for unknown reasons
 file(GLOB_RECURSE LEANLAKETESTS
   #"${LEAN_SOURCE_DIR}/lake/tests/test.sh"
   "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
-  if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online|buildArgs|badImport).*")
+  if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")
     GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
     GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
     add_test(NAME "leanlaketest_${DIR_NAME}"