diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cd64aee299dd..0eaa9fefb689 100644
--- a/src/CMakeLists.txt
+++ b/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")
diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean
index b6d707a3c15e..4ff07f93786f 100644
--- a/src/Init/System/Platform.lean
+++ b/src/Init/System/Platform.lean
@@ -25,6 +25,10 @@ Checks whether the current platform is macOS.
 -/
 @[extern "lean_system_platform_osx"] opaque getIsOSX : Unit → Bool
 /--
+Checks whether the current platform is Linux.
+-/
+@[extern "lean_system_platform_linux"] opaque getIsLinux : Unit → Bool
+/--
 Checks whether the current platform is [Emscripten](https://emscripten.org/).
 -/
 @[extern "lean_system_platform_emscripten"] opaque getIsEmscripten : Unit → Bool
@@ -39,6 +43,11 @@ Is the current platform macOS?
 -/
 def isOSX : Bool := getIsOSX ()
 
+/--
+Is the current platform Linux?
+-/
+def isLinux : Bool := getIsLinux ()
+
 /--
 Is the current platform [Emscripten](https://emscripten.org/)?
 -/
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index e8f915fe8423..a99631315f57 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -613,6 +613,7 @@ open Lean.Parser.Command.InternalSyntax in
   let platforms :=
     (if System.Platform.isWindows then [" Windows"] else [])
     ++ (if System.Platform.isOSX then [" macOS"] else [])
+    ++ (if System.Platform.isLinux then [" Linux"] else [])
     ++ (if System.Platform.isEmscripten then [" Emscripten"] else [])
   logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
 
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 1266fd0bf409..7db657579daa 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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
diff --git a/src/lake/Lake/DSL/Syntax.lean b/src/lake/Lake/DSL/Syntax.lean
index 695212454088..017a556ea747 100644
--- a/src/lake/Lake/DSL/Syntax.lean
+++ b/src/lake/Lake/DSL/Syntax.lean
@@ -464,7 +464,7 @@ meta if System.Platform.isWindows then
 extern_lib winOnlyLib := ...
 else meta if System.Platform.isOSX then
 extern_lib macOnlyLib := ...
-else
+else meta if System.Platform.isLinux then
 extern_lib linuxOnlyLib := ...
 ```
 -/
diff --git a/src/runtime/platform.cpp b/src/runtime/platform.cpp
index fc970703ab31..4dc48e4d95fc 100644
--- a/src/runtime/platform.cpp
+++ b/src/runtime/platform.cpp
@@ -33,6 +33,14 @@ extern "C" LEAN_EXPORT uint8 lean_system_platform_osx(obj_arg) {
 #endif
 }
 
+extern "C" LEAN_EXPORT uint8 lean_system_platform_linux(obj_arg) {
+#if defined(__linux__) && !defined(LEAN_EMSCRIPTEN)
+    return 1;
+#else
+    return 0;
+#endif
+}
+
 extern "C" LEAN_EXPORT uint8 lean_system_platform_emscripten(obj_arg) {
 #if defined(LEAN_EMSCRIPTEN)
     return 1;
diff --git a/tests/lake/tests/precompileModules-importLake/Foo.lean b/tests/lake/tests/precompileModules-importLake/Foo.lean
new file mode 100644
index 000000000000..88ae26a0d815
--- /dev/null
+++ b/tests/lake/tests/precompileModules-importLake/Foo.lean
@@ -0,0 +1 @@
+import Foo.ImportLake
diff --git a/tests/lake/tests/precompileModules-importLake/Foo/ImportLake.lean b/tests/lake/tests/precompileModules-importLake/Foo/ImportLake.lean
new file mode 100644
index 000000000000..6be89aa02f21
--- /dev/null
+++ b/tests/lake/tests/precompileModules-importLake/Foo/ImportLake.lean
@@ -0,0 +1 @@
+import Lake.Util.Casing
diff --git a/tests/lake/tests/precompileModules-importLake/clean.sh b/tests/lake/tests/precompileModules-importLake/clean.sh
new file mode 100755
index 000000000000..333b50aba242
--- /dev/null
+++ b/tests/lake/tests/precompileModules-importLake/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json produced.out
diff --git a/tests/lake/tests/precompileModules-importLake/lakefile.toml b/tests/lake/tests/precompileModules-importLake/lakefile.toml
new file mode 100644
index 000000000000..742bd4243e43
--- /dev/null
+++ b/tests/lake/tests/precompileModules-importLake/lakefile.toml
@@ -0,0 +1,6 @@
+name = "precompileModules-importLake"
+precompileModules = true
+defaultTargets = ["Foo"]
+
+[[lean_lib]]
+name = "Foo"
diff --git a/tests/lake/tests/precompileModules-importLake/test.sh b/tests/lake/tests/precompileModules-importLake/test.sh
new file mode 100755
index 000000000000..95584df0ec22
--- /dev/null
+++ b/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