feat: add SONAMEs to shared libraries

src/CMakeLists.txt

@@ -559,9 +559,13 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
   string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
   string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
   string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,-soname=libInit_shared.so")
+  string(APPEND LEANSHARED_1_LINKER_FLAGS " -Wl,-soname=libleanshared_1.so")
+  string(APPEND LEANSHARED_2_LINKER_FLAGS " -Wl,-soname=libleanshared_2.so")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-soname=libleanshared.so")
   string(
     APPEND LAKESHARED_LINKER_FLAGS
-    " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
+    " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive -Wl,-soname=libLake_shared.so"
   )
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
 elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")

src/Init/System/Platform.lean

@@ -44,6 +44,11 @@ Is the current platform [Emscripten](https://emscripten.org/)?
 -/
 def isEmscripten : Bool := getIsEmscripten ()
 
+/--
+Is the current platform Linux?
+-/
+def isLinux : Bool := !isWindows && !isOSX && !isEmscripten
+
 /--
 Gets the LLVM target triple of the current platform, or `""` if this was missing when Lean was
 compiled.

src/lake/Lake/Build/Module.lean

@@ -213,12 +213,24 @@ def computeModuleDeps
     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
+  On Linux, dynlibs that use Lake symbols are linked against `libLake_shared.so` (`--as-needed`).
+  The runtime linker is not able to find `lib/lean/libLake_shared.so` on disk
+  because we do not set `LD_LIBRARY_PATH`,
+  and the `DT_RUNPATH` entry on `bin/lean` pointing to `lib/lean`
+  is ignored when resolving transitive dependencies.
+  So we load `libLake_shared.so` eagerly *in case it might be needed*
+  (we don't know whether it is needed because an imported `Lake.*` module
+  will not be present in `Module.transImports`).
+  TODO: load as dynlib instead of as plugin,
+  see https://github.com/leanprover/lean4/pull/14326
+
+  MacOS *can* resolve the dylib but needs a plugin to run initializers,
+  see https://github.com/leanprover/lean4/issues/7388
+  TODO: remove macOS case once initializers are compiled correctly,
+  see https://github.com/leanprover/lean4/issues/14359
   -/
-  if Platform.isOSX && !(plugins.isEmpty && dynlibs.isEmpty) then
-    plugins := plugins.push (← getLakeInstall).sharedDynlib
+  if (Platform.isLinux || Platform.isOSX) && !(plugins.isEmpty && dynlibs.isEmpty) then
+    plugins := plugins.insertIdx 0 (← getLakeInstall).sharedDynlib
   return {dynlibs, plugins}
 
 structure TransImportEntry where

tests/lake/tests/precompileModules-importLake/Foo.lean

@@ -0,0 +1 @@
+import Foo.ImportLake

tests/lake/tests/precompileModules-importLake/Foo/ImportLake.lean

@@ -0,0 +1 @@
+import Lake.Util.Casing

tests/lake/tests/precompileModules-importLake/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out

tests/lake/tests/precompileModules-importLake/lakefile.toml

@@ -0,0 +1,6 @@
+name = "precompileModules-importLake"
+precompileModules = true
+defaultTargets = ["Foo"]
+
+[[lean_lib]]
+name = "Foo"

tests/lake/tests/precompileModules-importLake/test.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Test that precompiled modules can import Lake.
+# Regression test for https://github.com/leanprover/lean4/issues/9420.
+test_run -v build Foo