From de0187ab8bcc9cb75eb3eb360c96d221d180fe57 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 29 Apr 2025 21:04:59 -0400 Subject: [PATCH] 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 | 2 +- src/lake/tests/externLib/test.sh | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) 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