diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index df70a9ef3d..52d8dda5cf 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -50,7 +50,7 @@ def processCommand : FrontendM Bool := do
   let ictx ← getInputContext
   let pstate ← getParserState
   let scope := cmdState.scopes.head!
-  let pmctx := { env := cmdState.env, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
+  let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let pos := ictx.fileMap.toPosition pstate.pos
   match profileit "parsing" pos fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
   | (cmd, ps, messages) =>
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index f3b6572312..01de5caf48 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -121,6 +121,7 @@ structure InputContext where
 /-- Input context derived from elaboration of previous commands. -/
 structure ParserModuleContext where
   env           : Environment
+  options       : Options
   -- for name lookup
   currNamespace : Name := Name.anonymous
   openDecls     : List OpenDecl := []
@@ -1704,8 +1705,8 @@ def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
   { fn := fun c s => categoryParserOfStackFn offset { c with prec := prec } s }
 
 unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s =>
-  match ctx.env.evalConstCheck Parser {} `Lean.Parser.Parser declName <|>
-        ctx.env.evalConstCheck Parser {} `Lean.Parser.TrailingParser declName with
+  match ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.Parser declName <|>
+        ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.TrailingParser declName with
   | Except.ok p    => p.fn ctx s
   | Except.error e => s.mkUnexpectedError s!"error running parser {declName}: {e}"
 
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 8d9329da77..00e3d12251 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -407,7 +407,7 @@ def mkParserState (input : String) : ParserState :=
 
 /- convenience function for testing -/
 def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "<input>") : Except String Syntax :=
-  let c := mkParserContext (mkInputContext input fileName) { env := env }
+  let c := mkParserContext (mkInputContext input fileName) { env := env, options := {} }
   let s := mkParserState input
   let s := whitespace c s
   let s := categoryParserFnImpl catName c s
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 32f651d031..bb045607ad 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -39,7 +39,7 @@ private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : St
 
 def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do
   let dummyEnv ← mkEmptyEnvironment
-  let ctx := mkParserContext inputCtx { env := dummyEnv }
+  let ctx := mkParserContext inputCtx { env := dummyEnv, options := {} }
   let ctx := Module.updateTokens ctx
   let s   := mkParserState ctx.input
   let s   := whitespace ctx s
@@ -107,7 +107,7 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext)
 
 partial def testParseModuleAux (env : Environment) (inputCtx : InputContext) (s : ModuleParserState) (msgs : MessageLog) (stxs  : Array Syntax) : IO (Array Syntax) :=
   let rec parse (state : ModuleParserState) (msgs : MessageLog) (stxs : Array Syntax) :=
-    match parseCommand inputCtx { env := env } state msgs with
+    match parseCommand inputCtx { env := env, options := {} } state msgs with
     | (stx, state, msgs) =>
       if isEOI stx then
         if msgs.isEmpty then
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 2a6b45cc10..9cda686758 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -236,9 +236,14 @@ def trailingNode.formatter (k : SyntaxNodeKind) (_ : Nat) (p : Formatter) : Form
     categoryParser.formatter `foo
 
 def parseToken (s : String) : FormatterM ParserState := do
-  let ctx ← read
-  let env ← getEnv
-  pure $ Parser.tokenFn { input := s, fileName := "", fileMap := FileMap.ofString "", prec := 0, env := env, tokens := ctx.table } (Parser.mkParserState s)
+  Parser.tokenFn {
+    input := s,
+    fileName := "",
+    fileMap := FileMap.ofString "",
+    prec := 0,
+    env := ← getEnv,
+    options := ← getOptions,
+    tokens := (← read).table } (Parser.mkParserState s)
 
 def pushTokenCore (tk : String) : FormatterM Unit := do
   if tk.toSubstring.dropRightWhile (fun s => s == ' ') == tk.toSubstring then
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index c31cb6c674..53dcd501d6 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -80,7 +80,7 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
   let inputCtx := Parser.mkInputContext contents "<input>";
   let cmdState := snap.toCmdState;
   let scope := cmdState.scopes.head!
-  let pmctx := { env := cmdState.env, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
+  let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let (cmdStx, cmdParserState, msgLog) :=
     Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog;
   let cmdPos := cmdStx.getHeadInfo.get!.pos.get!; -- TODO(WN): always `some`?
diff --git a/stage0/src/library/compiler/ir_interpreter.cpp b/stage0/src/library/compiler/ir_interpreter.cpp
index 5fde882707..c00e44e935 100644
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
@@ -48,7 +48,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include "util/option_declarations.h"
 
 #ifndef LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE
-#if LEAN_IS_STAGE0 == 1
+#if false
 // We already set `-Dinterpreter.prefer_native=false` in stdlib.make, but also set it here as a default when we use stage 0 in the editor
 #define LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE false
 #else