fixity fix

src/Lean/Elab/Tactic/Config.lean

@@ -12,6 +12,12 @@ import Lean.Linter.MissingDocs
 namespace Lean.Elab.Tactic
 open Meta Parser.Tactic Command
 
+-- We automatically disable the following option for `macro`s but this file contains factored-out
+-- `private def`s containing quotations that ultimately are used only in the final `macro`s. Thus
+-- we disable the option for the full file, which is always correct for code that is only run at
+-- compile time of the current stage.
+set_option internal.parseQuotWithCurrentStage false
+
 private structure ConfigItemView where
   ref : Syntax
   option : Ident

stage0/src/stdlib_flags.h

@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, true);
+    opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax