diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index e2e4de4243..6ce5a86cc2 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/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" diff --git a/src/lake/tests/externLib/test.sh b/src/lake/tests/externLib/test.sh index a3c730f96e..6786844fec 100755 --- a/src/lake/tests/externLib/test.sh +++ b/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