fix: lake: import Lake w/ precompiled modules on MacOS (#8383)

This PR fixes the use of `import Lake` with precompiled modules, which
was previously broken on MacOS.

Closes #7388.

Author: tydeu

src/lake/Lake/Build/Module.lean

@@ -186,6 +186,13 @@ def computeModuleDeps
       plugins := plugins.push impLib
     else
       dynlibs := dynlibs.push impLib
+  /-
+  On MacOS, Lake must be loaded as a plugin for
+  `import Lake` to work with precompiled modules.
+  https://github.com/leanprover/lean4/issues/7388
+  -/
+  if Platform.isOSX && !(plugins.isEmpty && dynlibs.isEmpty) then
+    plugins := plugins.push (← getLakeInstall).sharedDynlib
   return {dynlibs, plugins}
 
 /--

src/lake/Lake/Config/InstallPath.lean

@@ -8,6 +8,7 @@ prelude
 import Init.Control.Option
 import Init.Data.Option.Coe
 import Lean.Compiler.FFI
+import Lake.Config.Dynlib
 import Lake.Util.NativeLib
 import Lake.Config.Defaults
 
@@ -114,19 +115,26 @@ structure LakeInstall where
   srcDir := home
   binDir := home / defaultBuildDir / defaultBinDir
   libDir := home / defaultBuildDir / defaultLeanLibDir
-  sharedLib := libDir / nameToSharedLib "Lake"
+  sharedDynlib : Dynlib := {
+    name := "Lake"
+    path := libDir / nameToSharedLib "Lake"
+  }
   lake := binDir / lakeExe
   deriving Inhabited, Repr
 
+@[inline] def LakeInstall.sharedLib (self : LakeInstall) : FilePath :=
+  self.sharedDynlib.path
+
 /-- Construct a Lake installation co-located with the specified Lean installation. -/
 def LakeInstall.ofLean (lean : LeanInstall) : LakeInstall where
   home := lean.sysroot
   srcDir := lean.srcDir / "lake"
   binDir := lean.binDir
   libDir := lean.leanLibDir
-  sharedLib :=
+  sharedDynlib :=
     let lib := s!"libLake_shared.{sharedLibExt}"
-    if Platform.isWindows then lean.binDir / lib else lean.leanLibDir / lib
+    let path := if Platform.isWindows then lean.binDir / lib else lean.leanLibDir / lib
+    {name := "Lake_shared", path}
   lake := lean.binDir / lakeExe
 
 /-! ## Detection Functions -/

src/lake/tests/precompileLink/LakeTest.lean

@@ -0,0 +1,2 @@
+import Lake
+import Foo

src/lake/tests/precompileLink/lakefile.lean

@@ -14,3 +14,5 @@ lean_lib FooDepDep
 lean_exe orderTest
 
 lean_lib Downstream
+
+lean_lib LakeTest

src/lake/tests/precompileLink/test.sh

@@ -3,6 +3,10 @@ source ../common.sh
 
 ./clean.sh
 
+# Test that precompilation works with a Lake import
+# https://github.com/leanprover/lean4/issues/7388
+test_run -v build LakeTest
+
 # Test that the link & load order of precompiled libraries is correct
 # https://github.com/leanprover/lean4/issues/7790
 test_run -v exe orderTest