src/stdlib_flags.h

#include "util/options.h"

// [ ] Check box to force CI to test stage 2 and run update-stage0 on PR merge
// (any other change to this file will do the same; ALL changes should be made to the stage0/ copy)

namespace lean {
options get_option_overrides() {
    options opts;
    // see https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md#further-bootstrapping-complications
#if LEAN_IS_STAGE0 == 1
    // uncomment to generally avoid bootstrapping issues limited to proofs
    //opts = opts.update({"debug", "proofAsSorry"}, true);

    // uncomment to generally avoid bootstrapping issues in `omega` and `grind`
    //opts = opts.update({"debug", "terminalTacticsAsSorry"}, true);

    // uncomment for ABI-breaking changes affecting meta code;
    // see also next option!
    //opts = opts.update({"interpreter", "prefer_native"}, true);

    // comment out when enabling `prefer_native` should also affect use
    // of built-in parsers in quotations; this should usually be done, but setting
    // both to `true` may be necessary for handling non-builtin parsers with
    // builtin elaborators
    // TODO: make consistent across stages
    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);

    // changes to builtin parsers may also require uncommenting the following option if macros/syntax
    // with custom precheck hooks were affected
    //opts = opts.update({"quotPrecheck"}, false);
#endif
    return opts;
}
}