| #include "util/options.h" | |
| namespace lean { | |
| options get_default_options() { | |
| options opts; | |
| // see https://leanprover.github.io/lean4/doc/make/index.html#further-bootstrapping-complications | |
| #if LEAN_IS_STAGE0 == 1 | |
| // switch to `true` for ABI-breaking changes affecting meta code | |
| opts.update("interpreter.prefer_native", false); | |
| // switch to `true` for changing built-in parsers | |
| opts.update("internal.parseQuotWithCurrentStage", false); | |
| #endif | |
| return opts; | |
| } | |
| } |