Lake/Lean fails to build native libraries on Linux because it tries to load `libLake_shared.so`

[ineol]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In trying to compile a project that depends on Mathlib and that uses precompileModules, I get a build error on Linux (and not on Macos) because lean tries to load libLake_shared.so which is not available.

Steps to Reproduce

1. Create a project which depends on mathlib and imports it
2. enable native compilation with precompileModules
3. run lake build

Expected behavior:

lean compiles the library to a shared object.

Actual behavior:

Lean outputs the following error:

trace: .> LEAN_PATH=/home/ineol/Code/scratch/test/.lake/packages/Cli/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/batteries/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/Qq/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/aesop/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/importGraph/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/plausible/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/packages/mathlib/.lake/build/lib/lean:/home/ineol/Code/scratch/test/.lake/build/lib/lean /home/ineol/.elan/toolchains/leanprover--lean4---nightly-2025-07-17/bin/lean --tstack=400000 /home/ineol/Code/scratch/test/SSA.lean -o /home/ineol/Code/scratch/test/.lake/build/lib/lean/SSA.olean -i /home/ineol/Code/scratch/test/.lake/build/lib/lean/SSA.ilean -c /home/ineol/Code/scratch/test/.lake/build/ir/SSA.c --setup /home/ineol/Code/scratch/test/.lake/build/ir/SSA.setup.json --json
error: SSA.lean:1:0: error loading library, libLake_shared.so: cannot open shared object file: No such file or directory
error: Lean exited with code 1
Some required builds logged failures:

Versions

Lean (version 4.23.0-nightly-2025-07-17, x86_64-unknown-linux-gnu, commit 65abbd90bf076447c83c50e7873f01d083216ad4, Release)

Additional Information

Here are the files I used to hit the error:

lakefile.toml

name = "SSA"
precompileModules = true
defaultTargets = ["SSA"]
moreLeanArgs = ["--tstack=400000"]

[[require]]
name = "mathlib"
git = "https://github.com/ineol/mathlib4"
rev = "push-txqlwmpvtuto"

[[lean_lib]]
name = "SSA"

SSA.lean

import Mathlib

def main (args : List String) : IO UInt32 :=
  pure 0

Note that I used this fork of mathlib to work around another bug by not compiling a module.

[Vtec234]

The issue occurs when we import a library that depends on Lake. Here is a mathlib-free reproducer (also occurs on leanprover/lean4:nightly-2026-07-07).

lean-toolchain

leanprover/lean4:v4.32.0-rc1

lakefile.toml

name = "SSA"
precompileModules = true
defaultTargets = ["SSA"]

[[lean_lib]]
name = "SSA"

SSA.lean

import SSA.Mod

SSA/Mod.lean

import Lake.Util.Casing

[Vtec234]

Here's what's happening here.

• With precompileModules, when elaborating SSA we pass --plugin=.lake/build/lib/lean/SSA_SSA_Mod.so (SSA.Mod:dynlib) to Lean.
• This shared library links dynamically (DT_NEEDED) against libLake_shared.so. The dynamic linker needs to be able to resolve this.
• libLake_shared.so is present in toolchainDir/lib/lean, but we need to tell the dynamic linker where to find it. While toolchainDir/bin/lean does have a DT_RUNPATH entry set to $ORIGIN/../lib:$ORIGIN/../lib/lean, this is not transitive on Linux, namely, when resolving the dependencies of a shared object, the original executable's RUNPATH is not used.
  • Our rpath setup is the same on Mac (set on toolchainDir/bin/lean, not set on dynlibs) but we don't see this issue there because LC_RPATH is transitive.

There are a few potential solutions, but this will need input from @tydeu.

1. Just set LD_LIBRARY_PATH in lake env. I don't love this, since LD_LIBRARY_PATH is usually for ad-hoc overrides.
2. Set the rpath on all dynlib targets. I think this would have to be an absolute rpath, since libLake_shared.so does not have a stable location relative to the local build directory.
3. Place a "classic" DT_RPATH entry, which is transitive, on bin/lean instead of DT_RUNPATH.
4. Don't link against libLake_shared.so at all - load it via --load-dynlib instead. We already --plugin it on Mac, funnily enough since in my experiments removing that flag on Mac does not break any test, while adding it on Linux would fix this issue. I don't know if there's a reason for loading Lake via the system linker like we do. Lake is builtin, but it's also just a precompiled import in this case; we don't add linker entries for any user-provided precompiled imports.
5. Link toolchainDir/bin/lean against libLake_shared.so. Not seriously suggesting this since the Lean binary doesn't need it.