`#eval` of an `IO` action aborts `lean` (uncaught `lean::exception`, exit 134) when it reaches a non-`meta` import through a local definition

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
  (Searched for the error message and for meta import / interpreter; #14574 and #14697 are related but different, see Context.)
• 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”)
  (Tested locally with leanprover/lean4:nightly-2026-09-10, since the test case needs two module files.)

Description

Note: this entire report (except for this paragraph) was written by Claude Fable 5.1. I am new to lean and don't understand what "meta" does. It's possible this is not a bug, but an uncaught C++ exception seemed weird enough to me to be worth reporting.

In a module file, #eval of an IO action that uses, through a definition in the same file, a declaration from a module imported without meta makes lean abort with an uncaught C++ exception (std::terminate, exit code 134 / SIGABRT, plus a core dump when ulimit -c allows one) instead of reporting an error. The same situation with a pure #eval reports the error normally, and a direct reference in the #eval term is caught by the elaborator's meta check.

Context

Found while adding a file of #eval checks (run at build time) to a library that uses the module system: the first draft had import where meta import was needed, and lake build aborted and left a core dump instead of giving an error. No prior Zulip discussion.

Related but distinct: #14574 (a named meta initialize imported without meta) and #14697 (import all + public import lets a public meta def use a non-meta private def). Both end in an ordinary (interpreter) unknown declaration error. The points of this issue are that the check is also missing for declarations reached through same-file definitions of a #eval, and that on the IO path the resulting exception is not caught, so lean aborts.

Steps to Reproduce

1. Create a package with these three files (no dependencies).

   lakefile.toml:

   name = "mwe"
   
   [[lean_lib]]
   name = "A"
   
   [[lean_lib]]
   name = "B"
   

   A.lean:

   module
   
   public def k : Nat := 42
   

   B.lean:

   module
   
   import A
   
   def ks : Array Nat := #[k]
   
   def run : IO Unit := IO.println s!"{ks.size}"
   
   #eval run
   

2. Run lake build B.

Expected behavior: An ordinary error and exit code 1, as in the pure variant below (or, better, the elaborator's own message: "k is not accessible here; consider adding public meta import A").

Actual behavior:

✔ [2/4] Built A
✖ [3/4] Building B
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: (interpreter) IR of declaration 'k' not available; this may point to a missing `meta` check in a metaprogram
error: Lean exited with code 134

With ulimit -c unlimited, a core dump is left in the package root (the working directory of the lean process). It is sparse: apparent size about 10 GB, about 60 MB on disk.

Versions

#eval Lean.versionString: "4.33.1"; also reproduced, with identical output, on "4.35.0-nightly-2026-09-10" (commit 587587f23e88af64e9059e400b771b0db49f2a4b).
lean --version: Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release); Lake 5.0.0-src+819816b; toolchains installed with elan 4.2.4.
OS: Linux x86_64 (Debian, kernel 6.12).

Variants, each differing from B.lean in one respect (1–3 checked on both 4.33.1 and the nightly, 4–5 on 4.33.1):

1. Pure #eval (#eval ks.size instead of the IO action): the same message, but reported as an ordinary error, exit code 1:

   error: BPure.lean:7:0: (interpreter) IR of declaration 'k' not available; this may point to a missing `meta` check in a metaprogram
   

2. Direct reference (#eval k, no local definition): caught by the elaborator:

   error: BDirect.lean:5:0: Invalid `meta` definition `_eval`, `k` is not accessible here; consider adding `public meta import A`
   

3. Adding meta import A (alongside import A): works, prints 1.
4. A function instead of a constant in A.lean (public def foo (n : Nat) : Nat := n + 1, with def bar : Nat := foo 1 in B.lean and the IO action printing bar): aborts the same way, with this as the uncaught exception:

   Could not find native implementation of external declaration 'foo' (symbols 'lp_mwe_foo___boxed' or 'lp_mwe_foo').
   For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.
   

5. With @[expose] public def k : Nat := 42 the IO variant happens to work (presumably the literal is inlined), and so does an @[expose]d constant of a single-field structure. An @[expose]d constant of a two-field structure (structure S where a : Bool; b : Bool / def s : S := ⟨false, true⟩, with def ss : Array S := #[s] in B.lean) aborts as above.

Diagnosis so far, not investigated further: the meta-accessibility check for #eval appears to consider only the declarations referenced directly by the evaluated term, not those reached through definitions of the same file; the interpreter then throws lean::exception when it finds no IR for the imported declaration. On the pure evaluation path that exception is caught and turned into an error; on the IO path it escapes to std::terminate.

Impact

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

Reproduce the failure with lakefile.toml, A.lean, and B.lean by running lake build B, then compare the pure #eval and IO paths. Trace the #eval elaborator's meta-accessibility check and the interpreter handling for declarations reached through same-file definitions. Done means the case reports an ordinary error with exit code 1 instead of aborting with an uncaught exception.