diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean
index 9df1c63ada..e21b258d49 100644
--- a/src/lake/Lake/Build/Imports.lean
+++ b/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 _ =>
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index dacae2454c..a42d444dda 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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"
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 1c46515ad9..58642486ab 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/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
diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean
index 97fa559f79..e80cdd8f85 100644
--- a/src/lake/Lake/CLI/Serve.lean
+++ b/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 := {
diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh
index 228608800a..87c6dddfbc 100755
--- a/src/lake/tests/badImport/test.sh
+++ b/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
diff --git a/src/lake/tests/common.sh b/src/lake/tests/common.sh
index 56eed82f30..4f526b3f06 100644
--- a/src/lake/tests/common.sh
+++ b/src/lake/tests/common.sh
@@ -72,6 +72,8 @@ test_err() {
       echo "Lake unexpectedly succeeded."
       return 1
     fi
+  else
+    return 1
   fi
 }
 
diff --git a/src/lake/tests/precompileLink/Downstream.lean b/src/lake/tests/precompileLink/Downstream.lean
new file mode 100644
index 0000000000..a556160664
--- /dev/null
+++ b/src/lake/tests/precompileLink/Downstream.lean
@@ -0,0 +1,3 @@
+import Downstream.Import
+
+#eval greetingRef.get
diff --git a/src/lake/tests/precompileLink/Downstream/Import.lean b/src/lake/tests/precompileLink/Downstream/Import.lean
new file mode 100644
index 0000000000..de6e269cea
--- /dev/null
+++ b/src/lake/tests/precompileLink/Downstream/Import.lean
@@ -0,0 +1 @@
+import Foo
diff --git a/src/lake/tests/precompileLink/Foo/Baz.lean b/src/lake/tests/precompileLink/Foo/Baz.lean
index 022ecda8c5..ba10b5cc13 100644
--- a/src/lake/tests/precompileLink/Foo/Baz.lean
+++ b/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
diff --git a/src/lake/tests/precompileLink/Indirect.lean b/src/lake/tests/precompileLink/Indirect.lean
new file mode 100644
index 0000000000..de6e269cea
--- /dev/null
+++ b/src/lake/tests/precompileLink/Indirect.lean
@@ -0,0 +1 @@
+import Foo
diff --git a/src/lake/tests/precompileLink/lakefile.lean b/src/lake/tests/precompileLink/lakefile.lean
index ef9d4a929b..f46ebaa3a0 100644
--- a/src/lake/tests/precompileLink/lakefile.lean
+++ b/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
diff --git a/src/lake/tests/precompileLink/test.sh b/src/lake/tests/precompileLink/test.sh
index 84df75a03d..6c70d36c6d 100755
--- a/src/lake/tests/precompileLink/test.sh
+++ b/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
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 70847518c4..e218124ac7 100644
--- a/src/shell/CMakeLists.txt
+++ b/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}"