diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 26c0d3fc5a..5daa3973e4 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Prelude
+meta import Init.Prelude
 set_option linter.missingDocs true -- keep it documented
 
 /-!
diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 02aa32b17f..ceebc39f73 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -9,7 +9,7 @@ module
 
 prelude
 import Init.Tactics
-import Init.Meta
+meta import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index e775d6cfc3..c4d4b4f63a 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -8,7 +8,7 @@ notation, basic datatypes and type classes
 module
 
 prelude
-import Init.Prelude
+meta import Init.Prelude
 import Init.SizeOf
 set_option linter.missingDocs true -- keep it documented
 
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 610bd40a8b..3c3c2f5cbb 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -174,7 +174,7 @@ recommended_spelling "zero" for "0#n" in [BitVec.ofNat, «term__#__»]
 recommended_spelling "one" for "1#n" in [BitVec.ofNat, «term__#__»]
 
 /-- Unexpander for bitvector literals. -/
-@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
+@[app_unexpander BitVec.ofNat] meta def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
   | `($(_) $n $i:num) => `($i:num#$n)
   | _ => throw ()
 
@@ -183,7 +183,7 @@ scoped syntax:max term:max noWs "#'" noWs term:max : term
 macro_rules | `($i#'$p) => `(BitVec.ofNatLT $i $p)
 
 /-- Unexpander for bitvector literals without truncation. -/
-@[app_unexpander BitVec.ofNatLT] def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
+@[app_unexpander BitVec.ofNatLT] meta def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
   | `($(_) $i $p) => `($i#'$p)
   | _ => throw ()
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index b5455b50d6..76a8a5e919 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -9,6 +9,7 @@ prelude
 import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.List.Notation
+import Init.Data.Nat.Div.Basic
 
 @[expose] section
 
diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean
index 9d3380ac23..fa17b43a87 100644
--- a/src/Init/Data/List/Notation.lean
+++ b/src/Init/Data/List/Notation.lean
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Nat.Div.Basic
+meta import Init.Data.Nat.Div.Basic
 
 /-!
 # Notation for `List` literals.
diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean
index c8a3361f91..a3a97f56be 100644
--- a/src/Init/Data/Nat/Div/Basic.lean
+++ b/src/Init/Data/Nat/Div/Basic.lean
@@ -9,6 +9,7 @@ prelude
 import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
+meta import Init.MetaTypes
 
 @[expose] section
 
diff --git a/src/Init/Data/ToString/Macro.lean b/src/Init/Data/ToString/Macro.lean
index 1e8ee44ad4..3c16377932 100644
--- a/src/Init/Data/ToString/Macro.lean
+++ b/src/Init/Data/ToString/Macro.lean
@@ -6,8 +6,7 @@ Author: Leonardo de Moura
 module
 
 prelude
-import Init.Meta
-import Init.Data.ToString.Basic
+meta import Init.Meta
 
 syntax:max "s!" interpolatedStr(term) : term
 
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 95799f46f0..259d13ee83 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -7,6 +7,7 @@ Authors: Shreyas Srinivas, François G. Dorais, Kim Morrison
 module
 
 prelude
+meta import Init.Coe
 import Init.Data.Array.Lemmas
 import Init.Data.Array.MapIdx
 import Init.Data.Array.InsertIdx
diff --git a/src/Init/Grind/PP.lean b/src/Init/Grind/PP.lean
index 9e438aa15f..7e2cbf4a1e 100644
--- a/src/Init/Grind/PP.lean
+++ b/src/Init/Grind/PP.lean
@@ -20,13 +20,13 @@ set_option linter.unusedVariables false in
 def node_def (_ : Nat) {α : Sort u} {a : α} : NodeDef := .unit
 
 @[app_unexpander node_def]
-def nodeDefUnexpander : PrettyPrinter.Unexpander := fun stx => do
+meta def nodeDefUnexpander : PrettyPrinter.Unexpander := fun stx => do
   match stx with
   | `($_ $id:num) => return mkIdent <| Name.mkSimple $ "#" ++ toString id.getNat
   | _ => throw ()
 
 @[app_unexpander NodeDef]
-def NodeDefUnexpander : PrettyPrinter.Unexpander := fun _ => do
+meta def NodeDefUnexpander : PrettyPrinter.Unexpander := fun _ => do
   return mkIdent <| Name.mkSimple "NodeDef"
 
 end Lean.Grind
diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
index b1688589ea..f9213920df 100644
--- a/src/Init/Grind/Util.lean
+++ b/src/Init/Grind/Util.lean
@@ -57,25 +57,25 @@ theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nes
   subst h; apply HEq.refl
 
 @[app_unexpander nestedProof]
-def nestedProofUnexpander : PrettyPrinter.Unexpander := fun stx => do
+meta def nestedProofUnexpander : PrettyPrinter.Unexpander := fun stx => do
   match stx with
   | `($_ $p:term) => `(‹$p›)
   | _ => throw ()
 
 @[app_unexpander MatchCond]
-def matchCondUnexpander : PrettyPrinter.Unexpander := fun stx => do
+meta def matchCondUnexpander : PrettyPrinter.Unexpander := fun stx => do
   match stx with
   | `($_ $p:term) => `($p)
   | _ => throw ()
 
 @[app_unexpander EqMatch]
-def eqMatchUnexpander : PrettyPrinter.Unexpander := fun stx => do
+meta def eqMatchUnexpander : PrettyPrinter.Unexpander := fun stx => do
   match stx with
   | `($_ $lhs:term $rhs:term) => `($lhs = $rhs)
   | _ => throw ()
 
 @[app_unexpander offset]
-def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
+meta def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
   match stx with
   | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
   | _ => throw ()
@@ -88,7 +88,7 @@ many `NatCast.natCast` applications which is too verbose. We add the following
 unexpander to cope with this issue.
 -/
 @[app_unexpander NatCast.natCast]
-def natCastUnexpander : PrettyPrinter.Unexpander := fun stx => do
+meta def natCastUnexpander : PrettyPrinter.Unexpander := fun stx => do
   match stx with
   | `($_ $a:term) => `(↑$a)
   | _ => throw ()
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 014493e171..22a6220f20 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -13,6 +13,8 @@ import Init.MetaTypes
 import Init.Syntax
 import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
+meta import Init.Data.Array.Basic
+meta import Init.Syntax
 
 namespace Lean
 
@@ -1610,7 +1612,7 @@ macro (name := declareSimpLikeTactic) doc?:(docComment)?
     else
       pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
-    @[macro $tacName] def expandSimp : Macro := fun s => do
+    @[macro $tacName] meta def expandSimp : Macro := fun s => do
       let cfg ← `(optConfig| $cfg)
       let s := s.setKind $kind
       let s := s.setArg 0 (mkAtomFrom s[0] $tkn (canonical := true))
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index c98d3003ba..aa3071b4c3 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -8,7 +8,6 @@ Notation for operators defined at Prelude.lean
 module
 
 prelude
-import Init.Prelude
 import Init.Coe
 set_option linter.missingDocs true -- keep it documented
 
@@ -27,14 +26,14 @@ of a lean file. For example, `def foo := 1` is a `command`, as is
 `namespace Foo` and `end Foo`. Commands generally have an effect on the state of
 adding something to the environment (like a new definition), as well as
 commands like `variable` which modify future commands within a scope. -/
-def command : Category := {}
+meta def command : Category := {}
 
 /-- `term` is the builtin syntax category for terms. A term denotes an expression
 in lean's type theory, for example `2 + 2` is a term. The difference between
 `Term` and `Expr` is that the former is a kind of syntax, while the latter is
 the result of elaboration. For example `by simp` is also a `Term`, but it elaborates
 to different `Expr`s depending on the context. -/
-def term : Category := {}
+meta def term : Category := {}
 
 /-- `tactic` is the builtin syntax category for tactics. These appear after
 `by` in proofs, and they are programs that take in the proof context
@@ -44,28 +43,28 @@ a term of the expected type. For example, `simp` is a tactic, used in:
 example : 2 + 2 = 4 := by simp
 ```
 -/
-def tactic : Category := {}
+meta def tactic : Category := {}
 
 /-- `doElem` is a builtin syntax category for elements that can appear in the `do` notation.
 For example, `let x ← e` is a `doElem`, and a `do` block consists of a list of `doElem`s. -/
-def doElem : Category := {}
+meta def doElem : Category := {}
 
 /-- `structInstFieldDecl` is the syntax category for value declarations for fields in structure instance notation.
 For example, the `:= 1` and `| 0 => 0 | n + 1 => n` in `{ x := 1, f | 0 => 0 | n + 1 => n }` are in the `structInstFieldDecl` class. -/
-def structInstFieldDecl : Category := {}
+meta def structInstFieldDecl : Category := {}
 
 /-- `level` is a builtin syntax category for universe levels.
 This is the `u` in `Sort u`: it can contain `max` and `imax`, addition with
 constants, and variables. -/
-def level : Category := {}
+meta def level : Category := {}
 
 /-- `attr` is a builtin syntax category for attributes.
 Declarations can be annotated with attributes using the `@[...]` notation. -/
-def attr : Category := {}
+meta def attr : Category := {}
 
 /-- `stx` is a builtin syntax category for syntax. This is the abbreviated
 parser notation used inside `syntax` and `macro` declarations. -/
-def stx : Category := {}
+meta def stx : Category := {}
 
 /-- `prio` is a builtin syntax category for priorities.
 Priorities are used in many different attributes.
@@ -73,7 +72,7 @@ Higher numbers denote higher priority, and for example typeclass search will
 try high priority instances before low priority.
 In addition to literals like `37`, you can also use `low`, `mid`, `high`, as well as
 add and subtract priorities. -/
-def prio : Category := {}
+meta def prio : Category := {}
 
 /-- `prec` is a builtin syntax category for precedences. A precedence is a value
 that expresses how tightly a piece of syntax binds: for example `1 + 2 * 3` is
@@ -84,7 +83,7 @@ In addition to literals like `37`, there are some special named precedence level
 * `max` for the highest precedence used in term parsers (not actually the maximum possible value)
 * `lead` for the precedence of terms not supposed to be used as arguments
 and you can also add and subtract precedences. -/
-def prec : Category := {}
+meta def prec : Category := {}
 
 end Parser.Category
 
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 3df120dbe9..405f60fe1c 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -9,10 +9,11 @@ module
 
 prelude
 import Init.Data.ToString.Basic
-import Init.Data.Array.Subarray
 import Init.Conv
 import Init.Meta
 import Init.While
+meta import Init.Data.Option.Basic
+meta import Init.Data.Array.Subarray
 
 namespace Lean
 
@@ -142,13 +143,13 @@ macro tk:"calc" steps:calcSteps : conv =>
   `(conv| tactic => calc%$tk $steps)
 end Lean
 
-@[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Unit.unit] meta def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
 
-@[app_unexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
+@[app_unexpander List.nil] meta def unexpandListNil : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `([])
 
-@[app_unexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
+@[app_unexpander List.cons] meta def unexpandListCons : Lean.PrettyPrinter.Unexpander
   | `($(_) $x $tail) =>
     match tail with
     | `([])      => `([$x])
@@ -157,105 +158,105 @@ end Lean
     | _          => throw ()
   | _ => throw ()
 
-@[app_unexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
+@[app_unexpander List.toArray] meta def unexpandListToArray : Lean.PrettyPrinter.Unexpander
   | `($(_) [$xs,*]) => `(#[$xs,*])
   | _               => throw ()
 
-@[app_unexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Prod.mk] meta def unexpandProdMk : Lean.PrettyPrinter.Unexpander
   | `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
   | `($(_) $x $y)          => `(($x, $y))
   | _                      => throw ()
 
-@[app_unexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
+@[app_unexpander ite] meta def unexpandIte : Lean.PrettyPrinter.Unexpander
   | `($(_) $c $t $e) => `(if $c then $t else $e)
   | _                => throw ()
 
-@[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Eq.ndrec] meta def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
   | _             => throw ()
 
-@[app_unexpander Eq.rec] def unexpandEqRec : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Eq.rec] meta def unexpandEqRec : Lean.PrettyPrinter.Unexpander
   | `($(_) $m $h) => `($h ▸ $m)
   | _             => throw ()
 
-@[app_unexpander Exists] def unexpandExists : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Exists] meta def unexpandExists : Lean.PrettyPrinter.Unexpander
   | `($(_) fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
   | `($(_) fun $x:ident => $b)                     => `(∃ $x:ident, $b)
   | `($(_) fun ($x:ident : $t) => $b)              => `(∃ ($x:ident : $t), $b)
   | _                                              => throw ()
 
-@[app_unexpander Sigma] def unexpandSigma : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Sigma] meta def unexpandSigma : Lean.PrettyPrinter.Unexpander
   | `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) × $b)
   | _                                  => throw ()
 
-@[app_unexpander PSigma] def unexpandPSigma : Lean.PrettyPrinter.Unexpander
+@[app_unexpander PSigma] meta def unexpandPSigma : Lean.PrettyPrinter.Unexpander
   | `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) ×' $b)
   | _                                 => throw ()
 
-@[app_unexpander Subtype] def unexpandSubtype : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Subtype] meta def unexpandSubtype : Lean.PrettyPrinter.Unexpander
   | `($(_) fun ($x:ident : $type) => $p)  => `({ $x : $type // $p })
   | `($(_) fun $x:ident => $p)            => `({ $x // $p })
   | _                                     => throw ()
 
-@[app_unexpander TSyntax] def unexpandTSyntax : Lean.PrettyPrinter.Unexpander
+@[app_unexpander TSyntax] meta def unexpandTSyntax : Lean.PrettyPrinter.Unexpander
   | `($f [$k])  => `($f $k)
   | _           => throw ()
 
-@[app_unexpander TSyntaxArray] def unexpandTSyntaxArray : Lean.PrettyPrinter.Unexpander
+@[app_unexpander TSyntaxArray] meta def unexpandTSyntaxArray : Lean.PrettyPrinter.Unexpander
   | `($f [$k])  => `($f $k)
   | _           => throw ()
 
-@[app_unexpander Syntax.TSepArray] def unexpandTSepArray : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Syntax.TSepArray] meta def unexpandTSepArray : Lean.PrettyPrinter.Unexpander
   | `($f [$k] $sep)  => `($f $k $sep)
   | _                => throw ()
 
-@[app_unexpander GetElem.getElem] def unexpandGetElem : Lean.PrettyPrinter.Unexpander
+@[app_unexpander GetElem.getElem] meta def unexpandGetElem : Lean.PrettyPrinter.Unexpander
   | `($_ $array $index $_) => `($array[$index])
   | _ => throw ()
 
-@[app_unexpander getElem!] def unexpandGetElem! : Lean.PrettyPrinter.Unexpander
+@[app_unexpander getElem!] meta def unexpandGetElem! : Lean.PrettyPrinter.Unexpander
   | `($_ $array $index) => `($array[$index]!)
   | _ => throw ()
 
-@[app_unexpander getElem?] def unexpandGetElem? : Lean.PrettyPrinter.Unexpander
+@[app_unexpander getElem?] meta def unexpandGetElem? : Lean.PrettyPrinter.Unexpander
   | `($_ $array $index) => `($array[$index]?)
   | _ => throw ()
 
-@[app_unexpander Array.empty] def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.empty] meta def unexpandArrayEmpty : Lean.PrettyPrinter.Unexpander
   | _ => `(#[])
 
-@[app_unexpander Array.mkArray0] def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray0] meta def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander
   | _ => `(#[])
 
-@[app_unexpander Array.mkArray1] def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray1] meta def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1) => `(#[$a1])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray2] def unexpandMkArray2 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray2] meta def unexpandMkArray2 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2) => `(#[$a1, $a2])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray3] def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray3] meta def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2 $a3) => `(#[$a1, $a2, $a3])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray4] def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray4] meta def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2 $a3 $a4) => `(#[$a1, $a2, $a3, $a4])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray5] def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray5] meta def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2 $a3 $a4 $a5) => `(#[$a1, $a2, $a3, $a4, $a5])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray6] def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray6] meta def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2 $a3 $a4 $a5 $a6) => `(#[$a1, $a2, $a3, $a4, $a5, $a6])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray7] def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray7] meta def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7])
   | _ => throw ()
 
-@[app_unexpander Array.mkArray8] def unexpandMkArray8 : Lean.PrettyPrinter.Unexpander
+@[app_unexpander Array.mkArray8] meta def unexpandMkArray8 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7 $a8) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7, $a8])
   | _ => throw ()
 
@@ -360,13 +361,13 @@ namespace Lean
 
 /-- Unexpander for the `{ x }` notation. -/
 @[app_unexpander singleton]
-def singletonUnexpander : Lean.PrettyPrinter.Unexpander
+meta def singletonUnexpander : Lean.PrettyPrinter.Unexpander
   | `($_ $a) => `({ $a:term })
   | _ => throw ()
 
 /-- Unexpander for the `{ x, y, ... }` notation. -/
 @[app_unexpander insert]
-def insertUnexpander : Lean.PrettyPrinter.Unexpander
+meta def insertUnexpander : Lean.PrettyPrinter.Unexpander
   | `($_ $a { $ts:term,* }) => `({$a:term, $ts,*})
   | _ => throw ()
 
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index eace359b94..44cf919df0 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -695,7 +695,7 @@ syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
 A `simpArg` is either a `*`, `-lemma` or a simp lemma specification
 (which includes the `↑` `↓` `←` specifications for pre, post, reverse rewriting).
 -/
-def simpArg := simpStar.binary `orelse (simpErase.binary `orelse simpLemma)
+meta def simpArg := simpStar.binary `orelse (simpErase.binary `orelse simpLemma)
 
 /-- A simp args list is a list of `simpArg`. This is the main argument to `simp`. -/
 syntax simpArgs := " [" simpArg,* "]"
@@ -704,7 +704,7 @@ syntax simpArgs := " [" simpArg,* "]"
 A `dsimpArg` is similar to `simpArg`, but it does not have the `simpStar` form
 because it does not make sense to use hypotheses in `dsimp`.
 -/
-def dsimpArg := simpErase.binary `orelse simpLemma
+meta def dsimpArg := simpErase.binary `orelse simpLemma
 
 /-- A dsimp args list is a list of `dsimpArg`. This is the main argument to `dsimp`. -/
 syntax dsimpArgs := " [" dsimpArg,* "]"
diff --git a/src/Lean/Compiler.lean b/src/Lean/Compiler.lean
index e80bc9e7c5..355d6db74d 100644
--- a/src/Lean/Compiler.lean
+++ b/src/Lean/Compiler.lean
@@ -14,6 +14,7 @@ import Lean.Compiler.NeverExtractAttr
 import Lean.Compiler.IR
 import Lean.Compiler.CSimpAttr
 import Lean.Compiler.FFI
+import Lean.Compiler.MetaAttr
 import Lean.Compiler.NoncomputableAttr
 import Lean.Compiler.Main
 import Lean.Compiler.AtMostOnce -- TODO: delete after we port code generator to Lean
diff --git a/src/Lean/Compiler/MetaAttr.lean b/src/Lean/Compiler/MetaAttr.lean
new file mode 100644
index 0000000000..f7b0f89447
--- /dev/null
+++ b/src/Lean/Compiler/MetaAttr.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import Lean.EnvExtension
+
+namespace Lean
+
+builtin_initialize metaExt : TagDeclarationExtension ← mkTagDeclarationExtension
+
+/-- Marks in the environment extension that the given declaration has been declared by the user as `meta`. -/
+def addMeta (env : Environment) (declName : Name) : Environment :=
+  metaExt.tag env declName
+
+/-- Returns true iff the user has declared the given declaration as `meta`. -/
+def isMeta (env : Environment) (declName : Name) : Bool :=
+  metaExt.isTagged env declName
+
+/--
+Returns the IR phases of the given declaration that should be considered accessible. Does not take
+additional IR loaded for language server purposes into account.
+-/
+@[export lean_get_ir_phases]
+def getIRPhases (env : Environment) (declName : Name) : IRPhases := Id.run do
+  if !env.header.isModule then
+    return .all
+  match env.getModuleIdxFor? declName with
+  | some idx => if isMeta env declName then .comptime else env.header.modules[idx.toNat]?.map (·.irPhases) |>.get!
+  -- Allow `meta`->non-`meta` acesses in the same module
+  | none => if isMeta env declName then .comptime else .all
+
+end Lean
diff --git a/src/Lean/Elab/AuxDef.lean b/src/Lean/Elab/AuxDef.lean
index 995bc5b2b7..b5e6bca83b 100644
--- a/src/Lean/Elab/AuxDef.lean
+++ b/src/Lean/Elab/AuxDef.lean
@@ -32,5 +32,5 @@ def elabAuxDef : CommandElab
     let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
     elabCommand <|
       ← `($[$doc?:docComment]? $[$attrs?:attributes]?
-          def $(mkIdentFrom (mkNullNode suggestion) id (canonical := true)):ident : $ty := $body)
+          meta def $(mkIdentFrom (mkNullNode suggestion) id (canonical := true)):ident : $ty := $body)
   | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 854319f233..e8414abdde 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -10,6 +10,7 @@ import Lean.Elab.BindersUtil
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Elab.Match
+import Lean.Compiler.MetaAttr
 
 namespace Lean.Elab.Term
 open Meta
@@ -109,6 +110,7 @@ def declareTacticSyntax (tactic : Syntax) (name? : Option Name := none) : TermEl
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
                                        safety := DefinitionSafety.safe }
     addDecl decl
+    modifyEnv (addMeta · name)
     compileDecl decl
     return name
 
diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index 21375bd055..1601f68dc6 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/src/Lean/Elab/BuiltinEvalCommand.lean
@@ -206,7 +206,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
           to '{.ofConstName ``IO}' or '{.ofConstName ``CommandElabM}'."
       addAndCompileExprForEval declName r (allowSorry := bang)
       -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
-      let r ← toMessageData <$> evalConst t declName
+      let r ← toMessageData <$> evalConst t declName (checkMeta := !Elab.inServer.get (← getOptions))
       return { eval := pure r, printVal := some (← inferType e) }
   let (output, exOrRes) ← IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
     try
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 04e3f6c8f6..9dc6e3d2c4 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -56,13 +56,18 @@ inductive RecKind where
   | «partial» | «nonrec» | default
   deriving Inhabited
 
+/-- Codegen-relevant modifiers. -/
+inductive ComputeKind where
+  | regular | «meta» | «noncomputable»
+  deriving Inhabited
+
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
   /-- Input syntax, used for adjusting declaration range (unless missing) -/
   stx             : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩
   docString?      : Option (TSyntax ``Parser.Command.docComment) := none
   visibility      : Visibility := Visibility.regular
-  isNoncomputable : Bool := false
+  computeKind     : ComputeKind := .regular
   recKind         : RecKind := RecKind.default
   isUnsafe        : Bool := false
   attrs           : Array Attribute := #[]
@@ -77,14 +82,29 @@ def Modifiers.isProtected : Modifiers → Bool
   | _                                => false
 
 def Modifiers.isPartial : Modifiers → Bool
-  | { recKind := .partial, .. } => true
-  | _                           => false
+  | { recKind := .partial, .. }  => true
+  | _                            => false
+
+/--
+Whether the declaration is explicitly `partial` or should be considered as such via `meta`. In the
+latter case, elaborators should not produce an error if partialty is unnecessary.
+-/
+def Modifiers.isInferredPartial : Modifiers → Bool
+  | { recKind := .partial, .. }  => true
+  | { computeKind := .meta, .. } => true
+  | _                            => false
 
 def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false
 
-/-- Adds attribute `attr` in `modifiers`, at the end -/
+def Modifiers.isMeta (m : Modifiers) : Bool :=
+  m.computeKind matches .meta
+
+def Modifiers.isNoncomputable (m : Modifiers) : Bool :=
+  m.computeKind matches .noncomputable
+
+/-- Adds attribute `attr` in `modifiers` -/
 def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.push attr }
 
@@ -105,7 +125,7 @@ instance : ToFormat Modifiers := ⟨fun m =>
      | .regular   => []
      | .protected => [f!"protected"]
      | .private   => [f!"private"])
-    ++ (if m.isNoncomputable then [f!"noncomputable"] else [])
+    ++ (match m.computeKind with | .regular => [] | .meta => [f!"meta"] | .noncomputable => [f!"noncomputable"])
     ++ (match m.recKind with | RecKind.partial => [f!"partial"] | RecKind.nonrec => [f!"nonrec"] | _ => [])
     ++ (if m.isUnsafe then [f!"unsafe"] else [])
     ++ m.attrs.toList.map (fun attr => format attr)
@@ -127,18 +147,18 @@ section Methods
 
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
-/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
+/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `meta`, `noncomputable`, doc string)-/
 def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
   let docCommentStx := stx.raw[0]
   let attrsStx      := stx.raw[1]
   let visibilityStx := stx.raw[2]
-  let isNoncomputable :=
+  let computeKind   :=
     if stx.raw[3].isNone then
-      false
+      .regular
     else if stx.raw[3][0].getKind == ``Parser.Command.meta then
-      false  -- TODO: handle `meta` declarations
+      .meta
     else
-      true
+      .noncomputable
   let unsafeStx     := stx.raw[4]
   let recKind       :=
     if stx.raw[5].isNone then
@@ -159,9 +179,8 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
     | none       => pure #[]
     | some attrs => elabDeclAttrs attrs
   return {
-    stx, docString?, visibility, recKind, attrs,
+    stx, docString?, visibility, computeKind, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
-    isNoncomputable
   }
 
 /--
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 10691b3e5b..97e346e3f1 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -993,9 +993,12 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
   else DefKind.«def»
 
 def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := {
-  isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable
-  recKind         := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default
-  isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe
+  computeKind :=
+    if mainHeaders.any (·.modifiers.isNoncomputable) then .noncomputable
+    else if mainHeaders.any (·.modifiers.isMeta) then .meta
+    else .regular
+  recKind     := if mainHeaders.any fun h => h.modifiers.isInferredPartial then RecKind.partial else RecKind.default
+  isUnsafe    := mainHeaders.any fun h => h.modifiers.isUnsafe
 }
 
 /--
diff --git a/src/Lean/Elab/ParseImportsFast.lean b/src/Lean/Elab/ParseImportsFast.lean
index 83905b3f1a..366d1ee140 100644
--- a/src/Lean/Elab/ParseImportsFast.lean
+++ b/src/Lean/Elab/ParseImportsFast.lean
@@ -204,7 +204,7 @@ def main : Parser :=
   keywordCore "module" (fun _ s => s) (fun _ s => { s with isModule := true }) >>
   keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >>
   many (keywordCore "private" (setIsExported true) (setIsExported false) >>
-    keywordCore "meta" (setIsMeta true) (setIsMeta false) >>
+    keywordCore "meta" (setIsMeta false) (setIsMeta true) >>
     keyword "import" >>
     keywordCore "all" (setImportAll false) (setImportAll true) >>
     moduleIdent)
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 2f40ca27a6..9ae6132c9a 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.ShareCommon
+import Lean.Compiler.MetaAttr
 import Lean.Compiler.NoncomputableAttr
 import Lean.Util.CollectLevelParams
 import Lean.Util.NumObjs
@@ -123,6 +124,20 @@ private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
       -- let info
       logInfo <| MessageData.trace { cls := `theorem } m!"{d.name}" (#[sizeMsg] ++ constOccsMsg)
 
+-- TODO: should become part of the compiler to deal with erasure
+private def checkMeta (preDef : PreDefinition) : TermElabM Unit := do
+  preDef.value.forEach' fun e => do
+    if e.isAutoParam then
+      return false
+    if let .const c .. := e then
+      match getIRPhases (← getEnv) c, preDef.modifiers.isMeta with
+      | .runtime, true =>
+        throwError "Invalid meta definition, '{.ofConstName c}' must be `meta` to access"
+      | .comptime, false =>
+        throwError "Invalid definition, may not access `meta` declaration '{.ofConstName c}'"
+      | _, _ => pure ()
+    return true
+
 private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs (cache := cacheProofs) preDef
@@ -158,8 +173,11 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
     withSaveInfoContext do  -- save new env
       addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
-    if preDef.modifiers.isNoncomputable then
-      modifyEnv fun env => addNoncomputable env preDef.declName
+    match preDef.modifiers.computeKind with
+    | .meta          => modifyEnv (addMeta · preDef.declName)
+    | .noncomputable => modifyEnv (addNoncomputable · preDef.declName)
+    | _              => pure ()
+    checkMeta preDef
     if compile && shouldGenCodeFor preDef then
       compileDecl decl
     if applyAttrAfterCompilation then
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index bbdf0525a3..98fd2d37d2 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -326,13 +326,22 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
         else if preDefs.any (·.modifiers.isUnsafe) then
           addAndCompileUnsafe preDefs
           preDefs.forM (·.termination.ensureNone "unsafe")
-        else if preDefs.any (·.modifiers.isPartial) then
-          for preDef in preDefs do
-            if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
-              withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
-          addAndCompilePartial preDefs
-          preDefs.forM (·.termination.ensureNone "partial")
         else
+          if preDefs.any (·.modifiers.isInferredPartial) then
+            let mut isPartial := true
+            for preDef in preDefs do
+              if !(← whnfD preDef.type).isForall then
+                if preDef.modifiers.isPartial then
+                  withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
+                else
+                  -- `meta` should not imply `partial` in this case
+                  isPartial := false
+
+            if isPartial then
+              addAndCompilePartial preDefs
+              preDefs.forM (·.termination.ensureNone "partial")
+              continue
+
           ensureFunIndReservedNamesAvailable preDefs
           try
             checkCodomainsLevel preDefs
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 1e0f21691b..7a03db3e4f 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -273,7 +273,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
     let quotSymbol := "`(" ++ suffix ++ "| "
     let name := catName ++ `quot
     let cmd ← `(
-      @[term_parser] def $(mkIdent name) : Lean.ParserDescr :=
+      @[term_parser] meta def $(mkIdent name) : Lean.ParserDescr :=
         Lean.ParserDescr.node `Lean.Parser.Term.quot $(quote Lean.Parser.maxPrec)
           (Lean.ParserDescr.node $(quote name) $(quote Lean.Parser.maxPrec)
             (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
@@ -295,7 +295,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
   let attrName := catName.appendAfter "_parser"
   let catDeclName := ``Lean.Parser.Category ++ catName
   setEnv (← Parser.registerParserCategory (← getEnv) attrName catName catBehavior catDeclName)
-  let cmd ← `($[$docString?]? def $(mkIdentFrom stx[2] (`_root_ ++ catDeclName) (canonical := true)) : Lean.Parser.Category := {})
+  let cmd ← `($[$docString?]? meta def $(mkIdentFrom stx[2] (`_root_ ++ catDeclName) (canonical := true)) : Lean.Parser.Category := {})
   declareSyntaxCatQuotParser catName
   elabCommand cmd
 
@@ -396,10 +396,10 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
   let attrInstances := attrInstances.getD { elemsAndSeps := #[] }
   let attrInstances := attrInstances.push attrInstance
   let d ← if let some lhsPrec := lhsPrec? then
-    `($[$doc?:docComment]? @[$attrInstances,*] def $declName:ident : Lean.TrailingParserDescr :=
+    `($[$doc?:docComment]? @[$attrInstances,*] meta def $declName:ident : Lean.TrailingParserDescr :=
         ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
   else
-    `($[$doc?:docComment]? @[$attrInstances,*] def $declName:ident : Lean.ParserDescr :=
+    `($[$doc?:docComment]? @[$attrInstances,*] meta def $declName:ident : Lean.ParserDescr :=
         ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
   trace `Elab fun _ => d
   withMacroExpansion stx d <| elabCommand d
@@ -409,7 +409,7 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
   -- TODO: nonatomic names
   let (val, _) ← runTermElabM fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous
   let stxNodeKind := (← getCurrNamespace) ++ declName.getId
-  let stx' ← `($[$doc?:docComment]? def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
+  let stx' ← `($[$doc?:docComment]? meta def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
   withMacroExpansion stx stx' <| elabCommand stx'
 
 def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 74549680bb..21ae429546 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -139,6 +139,21 @@ structure ModuleData where
   entries         : Array (Name × Array EnvExtensionEntry)
   deriving Inhabited
 
+/-- Phases for which some IR is available for execution. -/
+inductive IRPhases where
+  /-- Available for execution in the final native code. -/
+  | runtime
+  /-- Available for execution during elaboration. -/
+  | comptime
+  /-- Available during run time and compile time. -/
+  | all
+deriving Inhabited, BEq, Repr
+
+/-- Import including information resulting from processing of the entire import DAG. -/
+structure EffectiveImport extends Import where
+  /-- Phases for which the import's IR is available. -/
+  irPhases : IRPhases
+
 /-- Environment fields that are not used often. -/
 structure EnvironmentHeader where
   /--
@@ -157,14 +172,22 @@ structure EnvironmentHeader where
   /-- Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management. -/
   regions      : Array CompactedRegion := #[]
   /--
-  Name of all imported modules (directly and indirectly).
-  The index of a module name in the array equals the `ModuleIdx` for the same module.
+  Direct and transitive imports. Modules are given with their effective import modifiers, not their
+  original ones. Each module is listed at most once. The index of a module in the array equals the
+  `ModuleIdx` for the same module.
   -/
-  moduleNames  : Array Name   := #[]
+  modules      : Array EffectiveImport := #[]
   /-- Module data for all imported modules. -/
   moduleData   : Array ModuleData := #[]
   deriving Nonempty
 
+/--
+Name of all imported modules (directly and indirectly).
+The index of a module name in the array equals the `ModuleIdx` for the same module.
+-/
+def EnvironmentHeader.moduleNames (header : EnvironmentHeader) : Array Name :=
+  header.modules.map (·.module)
+
 namespace Kernel
 
 structure Diagnostics where
@@ -1159,7 +1182,7 @@ def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
   | _ => false
 
 def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
-  env.header.moduleNames.findIdx? (· == moduleName)
+  env.header.modules.findIdx? (·.module == moduleName)
 
 end Environment
 
@@ -1819,7 +1842,7 @@ where
     else
       return env
 
-private structure ImportedModule extends Import where
+private structure ImportedModule extends EffectiveImport where
   /-- All loaded incremental compacted regions. -/
   parts     : Array (ModuleData × CompactedRegion)
 
@@ -1883,7 +1906,7 @@ private def findOLeanParts (mod : Name) : IO (Array System.FilePath) := do
 partial def importModulesCore
     (imports : Array Import) (isModule := false) (arts : NameMap ModuleArtifacts := {}) :
     ImportStateM Unit := do
-  go imports (importAll := true) (isExported := isModule)
+  go imports (importAll := true) (isExported := isModule) (isMeta := false)
   if isModule then
     for i in imports do
       if let some mod := (← get).moduleNameMap[i.module]?.bind (·.mainModule?) then
@@ -1928,7 +1951,7 @@ For implementation purposes, we represent elements in the lattice using two flag
 
 `none` then is represented by not visiting a module at all.
 -/
-where go (imports : Array Import) (importAll : Bool) (isExported : Bool) := do
+where go (imports : Array Import) (importAll isExported isMeta : Bool) := do
   for i in imports do
     -- `B = none`?
     if !(i.isExported || importAll) then
@@ -1937,13 +1960,17 @@ where go (imports : Array Import) (importAll : Bool) (isExported : Bool) := do
     let importAll := !isModule || (importAll && i.importAll)
     -- `B ≥ public`?
     let isExported := isExported && i.isExported
+    let irPhases := if isMeta || i.isMeta then .comptime else .runtime
     let goRec imports := do
-      go (importAll := importAll) (isExported := isExported) imports
+      go (importAll := importAll) (isExported := isExported) (isMeta := isMeta || i.isMeta) imports
     if let some mod := (← get).moduleNameMap[i.module]? then
       -- when module is already imported, bump flags
-      if importAll && !mod.importAll || isExported && !mod.isExported then
+      let importAll := importAll || mod.importAll
+      let isExported := isExported || mod.isExported
+      let irPhases := if irPhases == mod.irPhases then irPhases else .all
+      if importAll != mod.importAll || isExported != mod.isExported || irPhases != mod.irPhases then
         modify fun s => { s with moduleNameMap := s.moduleNameMap.insert i.module { mod with
-          importAll, isExported }}
+          importAll, isExported, irPhases }}
         -- bump entire closure
         if let some mod := mod.mainModule? then
           goRec mod.imports
@@ -1961,7 +1988,7 @@ where go (imports : Array Import) (importAll : Bool) (isExported : Bool) := do
     let some (baseMod, _) := parts[0]? | unreachable!
     goRec baseMod.imports
     modify fun s => { s with
-      moduleNameMap := s.moduleNameMap.insert i.module { i with importAll, isExported, parts }
+      moduleNameMap := s.moduleNameMap.insert i.module { i with importAll, isExported, irPhases, parts }
       moduleNames := s.moduleNames.push i.module
     }
 
@@ -2053,10 +2080,9 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
     extraConstNames := {}
     extensions      := exts
     header     := {
-      trustLevel, imports, moduleData
-      isModule
+      trustLevel, imports, moduleData, isModule
+      modules      := modules.map (·.toEffectiveImport)
       regions      := modules.flatMap (·.parts.map (·.2))
-      moduleNames  := s.moduleNames
     }
   }
   let publicConstants : ConstMap := SMap.fromHashMap publicConstantMap false
@@ -2198,12 +2224,27 @@ def displayStats (env : Environment) : IO Unit := do
     unless fmt.isNil do IO.println ("  " ++ toString (Format.nest 2 (extDescr.statsFn s.state)))
     IO.println ("  number of imported entries: " ++ toString (s.importedEntries.foldl (fun sum es => sum + es.size) 0))
 
-/--
-  Evaluate the given declaration under the given environment to a value of the given type.
-  This function is only safe to use if the type matches the declaration's type in the environment
-  and if `enableInitializersExecution` has been used before importing any modules. -/
 @[extern "lean_eval_const"]
-unsafe opaque evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
+private unsafe opaque evalConstCore (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
+
+@[extern "lean_get_ir_phases"]
+private opaque getIRPhases (env : Environment) (constName : Name) : IRPhases
+
+/--
+Evaluates the given declaration under the given environment to a value of the given type.
+This function is only safe to use if the type matches the declaration's type in the environment
+and if `enableInitializersExecution` has been used before importing any modules.
+
+If `checkMeta` is true (the default), the function checks that the constant is declared or imported
+as `meta` or otherwise fails with an error. It should only be set to `false` in cases where it is
+acceptable for code to work only in the language server, where more IR is loaded, such as in
+`#eval`.
+-/
+unsafe def evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) (checkMeta := true) : Except String α :=
+  if checkMeta && getIRPhases env constName == .runtime then
+    throw ("cannot evaluate non-`meta` constant '" ++ toString constName ++ "'")
+  else
+    evalConstCore α env opts constName
 
 private def throwUnexpectedType {α} (typeName : Name) (constName : Name) : ExceptT String Id α :=
   throw ("unexpected type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 1c5b5b008a..3baec1f626 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -420,7 +420,7 @@ where
         if let some (some processed) ← old.processedResult.get? then
           -- ...and the edit is after the second-next command (see note [Incremental Parsing])...
           if let some nextCom ← processed.firstCmdSnap.get? then
-            if let some nextNextCom ← processed.firstCmdSnap.get? then
+            if let some nextNextCom ← nextCom.nextCmdSnap?.bindM (·.get?) then
               if (← isBeforeEditPos nextNextCom.parserState.pos) then
                 -- ...go immediately to next snapshot
                 return (← unchanged old old.stx oldSuccess.parserState)
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index ead127f46e..344ae70b88 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -147,8 +147,8 @@ See also `Lean.matchConstStructure` for a less restrictive version.
         | _ => failK ()
       | _ => failK ()
 
-unsafe def evalConst [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (α) (constName : Name) : m α := do
-  ofExcept <| (← getEnv).evalConst α (← getOptions) constName
+unsafe def evalConst [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (α) (constName : Name) (checkMeta := true) : m α := do
+  ofExcept <| (← getEnv).evalConst (checkMeta := checkMeta) α (← getOptions) constName
 
 unsafe def evalConstCheck [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (α) (typeName : Name) (constName : Name) : m α := do
   ofExcept <| (← getEnv).evalConstCheck α (← getOptions) typeName constName
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..6b964da742 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -11,7 +11,7 @@ options get_default_options() {
     opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with
diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out
index 98fd14c4eb..f11da383fb 100644
--- a/tests/lean/syntaxPrec.lean.expected.out
+++ b/tests/lean/syntaxPrec.lean.expected.out
@@ -1,6 +1,6 @@
 syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
 [Elab.command] @[term_parser 1000]
-    def «termFoo*_» : Lean.ParserDescr✝ :=
+    meta def «termFoo*_» : Lean.ParserDescr✝ :=
       ParserDescr.node✝ `«termFoo*_» 1022
         (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
           (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))