Interpreter error when importing named `meta initialize`

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

A named meta initialize, e.g. meta initialize foo : Unit ← do dbg_trace "hello" defined in module Foo, then imported via import Foo in module Bar, will cause lake build to emit an interpreter error.

With module names replaced for clarity:

% lake build Bar
✖ [3/3] Building Bar
trace: [...]
error: Bar.lean:1:0: (interpreter) unknown declaration '_private.Foo.0.foo'
info: stderr:
hello
error: Lean exited with code 1
Some required targets logged failures:
- Bar
error: build failed

Steps to Reproduce

1. Create two files in some project:

Foo:

module

meta initialize foo : Unit ← do dbg_trace "hello"

Bar:

module

import Foo

2. run lake build Bar

Expected behavior: The same behavior as meta initialize do dbg_trace "hello"; currently, this prints hello without error.

Actual behavior: error: Bar.lean:1:0: (interpreter) unknown declaration '_private.Foo.0.foo', and printing hello

Versions

4.34.0-nightly-2026-07-27, macOS

Additional Information

Doing any of the following fixes it:

• using an anonymous meta initialize do dbg_trace "hello", which prints hello and does not create the offending opaque foo in the first place
• using (public) meta import Foo with any modifiers on initialize, which always prints hello
• using public meta initialize, which prints hello (I'm thinking due to passing a certain guard during IR generation or export)
• using initialize or public initialize, which does not get run (does not print hello) since it's now just a runtime initializer
• creating a private meta def useFoo := foo in the same module (Foo), which prints hello

Reported on zulip here and independently earlier here.

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 the two modules Foo and Bar described in the issue, then run lake build Bar and compare named and anonymous meta initialize declarations. Trace the interpreter or import path responsible for the unknown private declaration. Done means the named form imports and builds like the anonymous form without the interpreter error.