diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 4fefad1773..f5a8a6c056 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -72,7 +72,7 @@ rec {
         src = ../src;
         fullSrc = ../.;
         inherit debug;
-        leanFlags = [ "-Dinterpreter.prefer_native=false" ];
+        leanFlags = [ "-Dinterpreter.prefer_native=true" ];
       });
     in (all: all // all.lean) rec {
       Init = build { name = "Init"; deps = []; };
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 73cde06e62..b231f5c83a 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -132,7 +132,7 @@ structure ParserModuleContext where
 structure ParserContext extends InputContext, ParserModuleContext where
   prec               : Nat
   tokens             : TokenTable
-  insideQuot         : Bool := false
+  quotDepth          : Nat := 0
   suppressInsideQuot : Bool := false
   savedPos?          : Option String.Pos := none
   forbiddenTk?       : Option Token := none
@@ -447,7 +447,7 @@ def setLhsPrecFn (prec : Nat) : ParserFn := fun c s =>
 }
 
 def checkInsideQuotFn : ParserFn := fun c s =>
-  if c.insideQuot then s
+  if c.quotDepth > 0 && !c.suppressInsideQuot then s
   else s.mkUnexpectedError "unexpected syntax outside syntax quotation"
 
 @[inline] def checkInsideQuot : Parser := {
@@ -456,7 +456,7 @@ def checkInsideQuotFn : ParserFn := fun c s =>
 }
 
 def checkOutsideQuotFn : ParserFn := fun c s =>
-  if !c.insideQuot then s
+  if !c.quotDepth == 0 || c.suppressInsideQuot then s
   else s.mkUnexpectedError "unexpected syntax inside syntax quotation"
 
 @[inline] def checkOutsideQuot : Parser := {
@@ -464,13 +464,17 @@ def checkOutsideQuotFn : ParserFn := fun c s =>
   fn   := checkOutsideQuotFn
 }
 
-def toggleInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
-  if c.suppressInsideQuot then p c s
-  else p { c with insideQuot := !c.insideQuot } s
+def addQuotDepthFn (i : Int) (p : ParserFn) : ParserFn := fun c s =>
+  p { c with quotDepth := c.quotDepth + i |>.toNat } s
 
-@[inline] def toggleInsideQuot (p : Parser) : Parser := {
+@[inline] def incQuotDepth (p : Parser) : Parser := {
   info := p.info,
-  fn   := toggleInsideQuotFn p.fn
+  fn   := addQuotDepthFn 1 p.fn
+}
+
+@[inline] def decQuotDepth (p : Parser) : Parser := {
+  info := p.info,
+  fn   := addQuotDepthFn (-1) p.fn
 }
 
 def suppressInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
@@ -1687,7 +1691,7 @@ def pushNone : Parser :=
   { fn := fun c s => s.pushSyntax mkNullNode }
 
 -- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
-def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> toggleInsideQuot termParser >> symbolNoAntiquot ")")
+def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
 def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
 @[inline] def tokenWithAntiquotFn (p : ParserFn) : ParserFn := fun c s => do
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 15f7169cab..d0c3749aee 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -15,7 +15,7 @@ namespace Parser
   Multiple command will be put in a `null node, but a single command will not (so that you can directly
   match against a quotation in a command kind's elaborator). -/
 -- TODO: use two separate quotation parsers with parser priorities instead
-@[builtinTermParser] def Term.quot := leading_parser "`(" >> toggleInsideQuot (termParser <|> many1Unbox commandParser) >> ")"
+@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth (termParser <|> many1Unbox commandParser) >> ")"
 @[builtinTermParser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
 
 namespace Command
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index d665ab1716..d674790317 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -125,7 +125,7 @@ The second `notFollowedBy` prevents this problem.
 
 @[builtinTermParser] def «do»  := leading_parser:argPrec "do " >> doSeq
 
-@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> toggleInsideQuot doElemParser >> ")"
+@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> incQuotDepth doElemParser >> ")"
 
 /- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/
 @[builtinTermParser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 8269b98793..e01c29f5c4 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -536,7 +536,7 @@ def notFollowedByCategoryTokenFn (catName : Name) : ParserFn := fun ctx s =>
     let (s, stx) := peekToken ctx s
     match stx with
     | Except.ok (Syntax.atom _ sym) =>
-      if ctx.insideQuot && sym == "$" then s
+      if ctx.quotDepth > 0 && sym == "$" then s
       else match cat.tables.leadingTable.find? (Name.mkSimple sym) with
       | some _ => s.mkUnexpectedError (toString catName)
       | _      => s
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 5833ba29d4..2681ed4d6b 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -42,9 +42,9 @@ end Syntax
 
 namespace Term
 
-@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|"  >> toggleInsideQuot syntaxParser >> ")"
-@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|"  >> toggleInsideQuot precedenceParser >> ")"
-@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|"  >> toggleInsideQuot priorityParser >> ")"
+@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|"  >> incQuotDepth syntaxParser >> ")"
+@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|"  >> incQuotDepth precedenceParser >> ")"
+@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|"  >> incQuotDepth priorityParser >> ")"
 
 end Term
 
@@ -76,9 +76,9 @@ def macroArgSimple := leading_parser ident >> checkNoWsBefore "no space before '
 def macroArgSymbol := leading_parser strLit >> optional (atomic <| checkNoWsBefore >> "%" >> checkNoWsBefore >> ident)
 def macroArg  := macroArgSymbol <|> atomic macroArgSimple
 def macroHead := macroArg
-def macroTailTactic   : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
-def macroTailCommand  : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
-def macroTailDefault  : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
+def macroTailTactic   : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> incQuotDepth Tactic.seq1 >> ")" <|> termParser)
+def macroTailCommand  : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> incQuotDepth (many1Unbox commandParser) >> ")" <|> termParser)
+def macroTailDefault  : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> incQuotDepth (categoryParserOfStack 2) >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
 @[builtinCommandParser] def «macro»       := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)
 
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 9cc5e166e0..f100848810 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -226,11 +226,11 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
 
 -- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
-@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|"  >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
+@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|"  >> incQuotDepth (evalInsideQuot ``funBinder funBinder) >> ")"
 def bracketedBinderF := bracketedBinder  -- no default arg
-@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|"  >> toggleInsideQuot (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
-@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|"  >> toggleInsideQuot (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
-@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|"  >> toggleInsideQuot attrParser >> ")"
+@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|"  >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")"
+@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|"  >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")"
+@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|"  >> incQuotDepth attrParser >> ")"
 
 @[builtinTermParser] def panic       := leading_parser:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := leading_parser:leadPrec "unreachable!"
@@ -245,14 +245,14 @@ def macroLastArg   := macroDollarArg <|> macroArg
 -- Macro for avoiding exponentially big terms when using `STWorld`
 @[builtinTermParser] def stateRefT   := leading_parser "StateRefT" >> macroArg >> macroLastArg
 
-@[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> toggleInsideQuot (parserOfStack 1) >> ")"
+@[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
 
 end Term
 
-@[builtinTermParser default+1] def Tactic.quot    : Parser := leading_parser "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
-@[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
+@[builtinTermParser default+1] def Tactic.quot    : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"
+@[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> incQuotDepth Tactic.seq1 >> ")"
 
-@[builtinTermParser] def Level.quot  : Parser := leading_parser "`(level|" >> toggleInsideQuot levelParser >> ")"
+@[builtinTermParser] def Level.quot  : Parser := leading_parser "`(level|" >> incQuotDepth levelParser >> ")"
 
 builtin_initialize
   register_parser_alias "letDecl"         Term.letDecl
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index b34f57a857..63d7f66db3 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -412,7 +412,8 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinatorFormatter Lean.Parser.setExpected]
 def setExpected.formatter (expected : List String) (p : Formatter) : Formatter := p
 
-@[combinatorFormatter Lean.Parser.toggleInsideQuot] def toggleInsideQuot.formatter (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (declName : Name) (p : Formatter) : Formatter := p
 
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index dc6d5df08d..a47898ef0e 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -465,7 +465,8 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
 @[combinatorParenthesizer Lean.Parser.setExpected]
 def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer := p
 
-@[combinatorParenthesizer Lean.Parser.toggleInsideQuot] def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (declName : Name) (p : Parenthesizer) : Parenthesizer := p
 
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 0488c50c2b..d055530d60 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -14,7 +14,7 @@ LEANMAKE_OPTS=\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
 	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
+	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=true"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
 	MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\