chore: update stage0

leanprover · Nov 7, 2024 · e0d72c6 · e0d72c6
1 parent 7cd6fbd
commit e0d72c6
Show file tree

Hide file tree

Showing 59 changed files with 60,558 additions and 52,665 deletions.
diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
@@ -6,9 +6,9 @@ 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);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // toggling `parseQuotWithCurrentStage` 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/stdlib/Init/Data/Array/Lemmas.c b/stage0/stdlib/Init/Data/Array/Lemmas.c
diff --git a/stage0/stdlib/Init/Data/Fin/Fold.c b/stage0/stdlib/Init/Data/Fin/Fold.c