From 294f7fbec5126ec99117a775bf9408ee94d9b8c2 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 27 Jun 2024 11:08:52 -0400
Subject: [PATCH] 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         |  9 +++++----
 src/lake/examples/ffi/app/lakefile.lean |  3 ++-
 src/lake/examples/ffi/lib/lakefile.lean |  7 +++----
 src/lake/examples/ffi/package.sh        | 10 ----------
 src/lake/examples/ffi/test.sh           | 16 +++++++++++++---
 5 files changed, 23 insertions(+), 22 deletions(-)
 delete mode 100755 src/lake/examples/ffi/package.sh

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 7e4edbdcf7..03ca79436b 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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
 
diff --git a/src/lake/examples/ffi/app/lakefile.lean b/src/lake/examples/ffi/app/lakefile.lean
index 49d321fccf..4d41977d6d 100644
--- 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
index 7191a47304..18d3af36f9 100644
--- 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
deleted file mode 100755
index 29a138c842..0000000000
--- a/src/lake/examples/ffi/package.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-set -ex
-
-cd app
-${LAKE:-../../../.lake/build/bin/lake} build -v -U
-cd ..
-
-
-cd lib
-${LAKE:-../../../.lake/build/bin/lake} build -v
-cd ..
diff --git a/src/lake/examples/ffi/test.sh b/src/lake/examples/ffi/test.sh
index 0b1651f6cd..f8561274e7 100755
--- 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