fix: lake: extern_lib loading in non-precompiled module builds (#8152)

This PR fixes a regression where non-precompiled module builds would
`--load-dynlib` package `extern_lib` targets.

A reappearance of #4565. Thanks to Daniil [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Multiple.20extern_lib/near/514772675)
for the report! This was not caught by the old test due to the removal
of `extern_lib` from the FFI example.

src/lake/Lake/Build/Module.lean

@@ -218,7 +218,7 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
   let impLibsJob ← Job.collectArray (traceCaption := "import dynlibs") <$>
     mod.fetchImportLibs precompileImports mod.shouldPrecompile
   let externLibsJob ← Job.collectArray (traceCaption := "package external libraries") <$>
-    mod.pkg.externLibs.mapM (·.dynlib.fetch)
+    if mod.shouldPrecompile then mod.pkg.externLibs.mapM (·.dynlib.fetch) else pure #[]
   let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg "module dynlibs"
   let pluginsJob ← mod.plugins.fetchIn mod.pkg "module plugins"
 

src/lake/tests/externLib/test.sh

@@ -12,5 +12,10 @@ test_run -v build Test
 # Tests the successful compilation of an `extern_lib` from a dep
 test_run -v exe test
 
+# Tests that a non-precompiled build does not load anything as a dynlib/plugin
+# https://github.com/leanprover/lean4/issues/4565
+$LAKE -v build test | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
+$LAKE -v -d ffi build test | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
+
 # Cleanup
 rm -f produced.out