chore: default parseQuotWithCurrentStage to true in stage 0

leanprover · Nov 25, 2024 · 620ead5 · 620ead5
1 parent 884a9ea
commit 620ead5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 6 deletions.
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
@@ -7,9 +7,10 @@ options get_default_options() {
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
-    // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
-    // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
+    // switch to `false` when enabling `prefer_native` should also affect use
+    // of built-in parsers in quotations
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    // changes to built-in parsers may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);
 

diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
@@ -7,9 +7,10 @@ options get_default_options() {
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
-    // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
-    // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
+    // switch to `false` when enabling `prefer_native` should also affect use
+    // of built-in parsers in quotations
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    // changes to built-in parsers may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);