fix: lake: computation of precompiled libs

leanprover · Jun 26, 2024 · a051669 · a051669
1 parent e3578c2
commit a051669
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 22 deletions.
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
@@ -108,12 +108,17 @@ 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 ← try mod.precompileImports.fetch
+  let precompileImports ←
+    try
+      if mod.shouldPrecompile then
+        mod.transImports.fetch
+      else
+        mod.precompileImports.fetch
     catch errPos => return Job.error (← takeLogFrom errPos)
   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
 

diff --git a/src/lake/examples/ffi/app/lakefile.lean b/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
diff --git a/src/lake/examples/ffi/lib/lakefile.lean b/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

diff --git a/src/lake/examples/ffi/package.sh b/src/lake/examples/ffi/package.sh
diff --git a/src/lake/examples/ffi/test.sh b/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