chore: update stage0

leanprover · Jan 19, 2025 · 74bd40d · 74bd40d
1 parent 4213862
commit 74bd40d
Show file tree

Hide file tree

Showing 254 changed files with 9,549 additions and 6,540 deletions.
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
@@ -9,7 +9,7 @@ options get_default_options() {
     opts = opts.update({"debug", "proofAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, true);
+    opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with

diff --git a/stage0/stdlib/Init/Tactics.c b/stage0/stdlib/Init/Tactics.c
diff --git a/stage0/stdlib/Lake/CLI/Translate.c b/stage0/stdlib/Lake/CLI/Translate.c