blob: 37aa19a850b5d9b29ec23ad1114928ed1852f401 [file] [edit]
#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;
}
}