fix: evalConst meta check and auxiliary IR decls (#11079)

Uncovered in Mathlib through new boxed decls from `BaseIO` changes

src/Lean/Compiler/IR/CompilerM.lean

@@ -159,21 +159,23 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
   #[(declMapExt.name, irEntries),
     (Lean.regularInitAttr.ext.name, initDecls)]
 
-@[export lean_ir_find_env_decl]
-def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
+def findEnvDecl (env : Environment) (declName : Name) (includeServer := false): Option Decl :=
   match env.getModuleIdxFor? declName with
   | some modIdx =>
-    -- `meta import/import all` and server `#eval`
-    -- This case is important even for codegen because it needs to see IR via `import all` (because
-    -- it can also see the LCNF)
+    -- `meta import/import all` and, optionally, additional server-mode IR
+    guard (includeServer || env.header.modules[modIdx]?.any (·.irPhases != .runtime)) *>
     findAtSorted? (declMapExt.getModuleIREntries env modIdx) declName <|>
     -- (closure of) `meta def`; will report `.extern`s for other `def`s so needs to come second
     findAtSorted? (declMapExt.getModuleEntries env modIdx) declName
   | none => declMapExt.getState env |>.find? declName
 
-/-- Like ``findEnvDecl env (declName ++ `_boxed)`` but with optimized negative lookup. -/
+@[export lean_ir_find_env_decl]
+private def findInterpDecl (env : Environment) (declName : Name) : Option Decl :=
+  findEnvDecl (includeServer := true) env declName
+
+/-- Like ``findInterpDecl env (declName ++ `_boxed)`` but with optimized negative lookup. -/
 @[export lean_ir_find_env_decl_boxed]
-private def findEnvDeclBoxed (env : Environment) (declName : Name) : Option Decl :=
+private def findInterpDeclBoxed (env : Environment) (declName : Name) : Option Decl :=
   let boxed := declName ++ `_boxed
   -- Important: get module index of base name, not boxed version. Usually the interpreter never
   -- does negative lookups except in the case of `call_boxed` which must check whether a boxed

src/Lean/Compiler/IR/Meta.lean

@@ -66,7 +66,10 @@ where go (ref : Name) : StateT NameSet (Except String) Unit := do
       for ref in collectUsedFDecls localDecl do
         go ref
     else
-      if getIRPhases env ref == .runtime then
+      -- NOTE: We do not use `getIRPhases` here as it's intended for env decls, nor IR decls. We do
+      -- not set `includeServer` as we want this check to be independent of server mode. Server-only
+      -- users disable this check instead.
+      if findEnvDecl env ref |>.isNone then
         throw s!"Cannot evaluate constant `{declName}` as it uses `{ref}` which is neither marked nor imported as `meta`"
 
 builtin_initialize

tests/pkg/module/Module/Basic.lean

@@ -2,6 +2,8 @@ module
 
 meta import Init.Dynamic
 meta import Init.System.IO
+public import Lean.PrettyPrinter.Delaborator.Basic
+public meta import Lean.PrettyPrinter.Delaborator.Basic
 
 public axiom testSorry : α
 
@@ -504,3 +506,10 @@ noncomputable section
 #guard_msgs in
 meta def m := S.s
 end
+
+-- setup for `Imported`
+public meta def delab : Lean.PrettyPrinter.Delaborator.Delab :=
+  default
+
+public def noMetaDelab : Lean.PrettyPrinter.Delaborator.Delab :=
+  default

tests/pkg/module/Module/Imported.lean

@@ -3,6 +3,7 @@ module
 prelude
 public import Module.Basic
 import Lean.DocString
+meta import Lean.Elab.Command
 
 /-! Definitions should be exported without their bodies by default -/
 
@@ -185,3 +186,20 @@ theorem f_struct_eq : f_struct 0 = 0 := by
 #guard_msgs in
 open Lean in
 #eval show CoreM _ from do findDocString? (← getEnv) ``pubInheritDoc
+
+/-! Cross-module `meta` checks, including involving compiler-introduced constants. -/
+
+attribute [local delab Nat] delab
+
+/--
+error: Cannot add attribute `[Lean.PrettyPrinter.Delaborator.delabAttribute]`: Declaration `noMetaDelab` must be marked as `meta`
+-/
+#guard_msgs in
+attribute [local delab Nat] noMetaDelab
+
+@[noinline] meta def pap (f : α → β) (a : α) : β := f a
+public meta def delab' : Lean.PrettyPrinter.Delaborator.Delab :=
+  pap delab
+
+-- Used to complain about `_boxed` not being meta
+attribute [local delab Nat] delab'