Unexpected compilation error "Could not find native implementation of external declaration"

Prerequisites

• 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

The following compilation error may appear on valid good:

error: M/B.lean:7:0: Could not find native implementation of external declaration 'f' (symbols 'lp_m_f___boxed' or 'lp_m_f').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

The error occurs when importing a file from another, only in the file importing, not in the one where the actual error appears.

Adding supportInterpreter = true in lakefile.toml does not change anything (including the hint, it's still there).

Context

I ran into this when porting old lean code to the new module system. The code I ported was using lean 4.31, but this error happens on the current nightly version too.
I believe this issue is related to meta/non-meta declarations.

Steps to Reproduce

1. Make a new lean project named M
2. Add the following files:
   A.lean

module
public def f (x : Nat) := x

B.lean

module
import M.A
public def g x := f x
#eval g 42

3. Import B.lean from the package root and run lake build.

Expected behavior:
This should build fine, or an error should inform the user how to import A.lean correctly for it to work, and it should appear when building B.lean by itself.

Actual behavior:
The following error appears when opening the the module root in the editor, or when running lake build.
The error does not appear when opening B.lean.

trace: .> LEAN_PATH=/Users/jr/delete-me/.lake/build/lib/lean /Users/jr/.elan/toolchains/leanprover--lean4-nightly---nightly-2026-08-30/bin/lean 
/Users/jr/delete-me/M/B.lean -o /Users/jr/delete-me/.lake/build/lib/lean/M/B.olean -i /Users/jr/delete-me/.lake/build/lib/lean/M/B.ilean -c /Use
rs/jr/delete-me/.lake/build/ir/M/B.c --setup /Users/jr/delete-me/.lake/build/ir/M/B.setup.json --json
error: M/B.lean:7:0: Could not find native implementation of external declaration 'f' (symbols 'lp_m_f___boxed' or 'lp_m_f').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakef
ile.lean`.
Some required targets logged failures:
- M.B
error: build failed

Versions

Lean 4.35.0-nightly-2026-08-30
Target: arm64-apple-darwin24.6.0 macOS

Additional Information

Adding meta import M.A in addition to import M.A fixes the issue.
And marking g as meta makes the errors behave in a sensible way, and helps the user fix the code.
The problem also happens when using #guard instead of #eval.

Impact

Perhaps this is a niche bug, but it was very confusing to solve, and completely stops you from being able to use Lean. I would imagine a user that simply wants to use #guard or #eval along with module and that does not know about meta at all would simply not be able to solve a case like this.

Start by reproducing the issue with the two minimal files, A.lean and B.lean, using lake build from the package root. Compare building B.lean alone with importing it from the module root, and inspect the import M.A, meta import M.A, #eval, and #guard cases. Done means valid code builds consistently or reports a clear correction at the relevant location.