Cross-package `#eval`/`#guard` failures: "IR of declaration

Stream: new members

[Kevin Sullivan]

Cross-package #eval/#guard failures: "IR of declaration not available"

I'm extracting a set of type definitions from package A (Designer) into a new package B (Schema). Package A depends on package B via a local path dependency. The definitions keep the same Lean namespaces — only the Lake package changed.

After the move, all proofs and non-#eval code works fine. But any #eval or #guard in package A that transitively calls a function now defined in package B fails with:

plaintext
(interpreter) IR of declaration 'Designer.Language.Signature.empty' not available;this may point to a missing `meta` check in a metaprogram

or:

plaintext
Could not find native implementation of external declaration 'Designer.Language.UUID.freshUUID'(symbols 'lp_Schema_Designer_Language_UUID_freshUUID___boxed' or'lp_Schema_Designer_Language_UUID_freshUUID')

The natural fix would be precompileModules = true on package B's lean_lib, but package B depends on Mathlib, and precompileModules cascades to dependencies. Linking all of Mathlib into a shared library fails (command line too long / clang error on macOS).
Question: Is there a way to make a library's IR available for cross-package interpretation without precompileModules, or a way to scope precompileModules to only the library's own modules (not its dependencies)?
Environment: Lean 4.27.0, macOS, Lake with moduleSystem = true

[Eric Wieser]

You should be using meta import in the files using #eval

[Kevin Sullivan]

I did manage to get this resolved. R's suggestion to have interpretation as well as precompilation enabled. That works. But now I'll go look at this approach, too. Thank you.