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

When building a project with precompileModules = true and a dependency on, say, Aesop, I get the following error:

✖ [610/612] Building Main
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/build/lib/lean /Users/ineol/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-04-01/bin/lean ././././Main.lean -R ./././. -o ././.lake/build/lib/lean/Main.olean -i ././.lake/build/lib/lean/Main.ilean -c ././.lake/build/ir/Main.c --plugin ././.lake/build/lib/libReprod.dylib --plugin ././.lake/packages/aesop/.lake/build/lib/libAesop.dylib --plugin ././.lake/packages/batteries/.lake/build/lib/libBatteries.dylib --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(/Users/ineol/Code/scratch/bug/.lake/packages/aesop/.lake/build/lib/libAesop.dylib, 0x0009): symbol not found in flat namespace '_l_Array_mergeDedup___rarg___lambda__1___boxed'
error: Lean exited with code 134

The issue (I think) is that that symbol is defined in the Batteries library, but it is given in a latter argument. If I permute the two -plugin arguments, the build succeeds.

This commit is probably the cause of the change of behavior.

cc @tydeu

Steps to Reproduce

The attached zip file contains the reduced test project.

1. Create a project with a recent enough Lean version (I used the April 1st nighlty)
2. Create the following lakefile.toml:

name = "reprod"
version = "0.1.0"
defaultTargets = ["reprod"]
precompileModules = true 

[[require]]
name = "aesop"
git = "https://github.com/leanprover-community/batteries"
rev = "master"

[[lean_lib]]
name = "Reprod"

[[lean_exe]]
name = "reprod"
root = "Main"

and import Aesop in Main.lean

3. Run lake build

Expected behavior: It compiles

Actual behavior: The build fails with the above error

Versions

With Lean version 4.19.0-nightly-2025-04-01

On MacOS

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.