Problem with `precompileModules = true`: `libLake_shared.so`

Stream: lean4

[Valentin Mikhalchuk]

When I set precompileModules = true in lakefile.lean, lake build fails with:

libc++abi: terminating due to uncaught exception of type lean::exception:
error loading library, libLake_shared.so: cannot open shared object file: No such file or directory

The file does exist at:

~/.elan/toolchains/leanprover--lean4---v4.20.0/lib/lean/libLake_shared.so

This only happens when precompileModules = true. Without it, the build completes normally.

There's an unanswered question on PA.SE with the same issue:
https://proofassistants.stackexchange.com/questions/5095/using-precompilemodules-and-mathlib-in-lakefile-causes-error-loading-library-l

I also couldn’t find anything useful in Zulip.

---

lakefile.lean:

import Lake
open Lake DSL

package testPrecompile where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩
  ]

require mathlib from
    git "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0"

@[default_target]
lean_lib TestPrecompile {
  precompileModules := true
}

Basic.lean:

import Mathlib.Tactic

def hello := "world"

---

Questions:

1. Why does precompileModules cause this shared library error?
2. How can I fix or work around it (e.g., by setting an environment variable)?