fix: lake: computation of precompiled libs (#4566)

Addresses a few issues with precompile library computation. 

* Fixes a bug where Lake would always precompile the package of a
module.
* If a module is precompiled, it now precompiles its imports.
Previously, it would only do this if imported.

Closes #4565.

src/lake/Lake/Build/Module.lean

@@ -107,11 +107,12 @@ def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array F
     if imp.name = mod.name then
       logError s!"{mod.leanFile}: module imports itself"
     imp.olean.fetch
-  let precompileImports ← mod.precompileImports.fetch
+  let precompileImports ← if mod.shouldPrecompile then
+    mod.transImports.fetch else mod.precompileImports.fetch
   let modLibJobs ← precompileImports.mapM (·.dynlib.fetch)
-  let pkgs := precompileImports.foldl (·.insert ·.pkg)
-    OrdPackageSet.empty |>.insert mod.pkg |>.toArray
-  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
+  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty
+  let pkgs := if mod.shouldPrecompile then pkgs.insert mod.pkg else pkgs
+  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs.toArray
   let externDynlibsJob ← BuildJob.collectArray externJobs
   let modDynlibsJob ← BuildJob.collectArray modLibJobs
 

src/lake/examples/ffi/app/lakefile.lean

@@ -9,4 +9,5 @@ require ffi from ".."/"lib"
 lean_exe app where
   root := `Main
 
-lean_lib Test
+lean_lib Test where
+  precompileModules := true

src/lake/examples/ffi/lib/lakefile.lean

@@ -1,14 +1,13 @@
 import Lake
 open System Lake DSL
 
-package ffi {
+package ffi where
   srcDir := "lean"
-  precompileModules := true
-}
 
 lean_lib FFI
 
-@[default_target] lean_exe test where
+@[default_target]
+lean_exe test where
   root := `Main
 
 target ffi.o pkg : FilePath := do

src/lake/examples/ffi/test.sh

@@ -1,8 +1,18 @@
-set -ex
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
-./package.sh
+
+# Tests that a non-precmpiled build does not load anything as a dynlib
+# https://github.com/leanprover/lean4/issues/4565
+$LAKE -d app build -v | (grep --color load-dynlib && exit 1 || true)
+$LAKE -d lib build -v | (grep --color load-dynlib && exit 1 || true)
+
 ./app/.lake/build/bin/app
 ./lib/.lake/build/bin/test
 
-${LAKE:-../../.lake/build/bin/lake} -d app build -v Test
+# Tests the successful precompilation of an `extern_lib`
+# Also tests a module with `precompileModules` always precompiles its imports
+$LAKE -d app build Test