chore: collect stdlib compilation flags in new header

doc/make/index.md

@@ -180,6 +180,11 @@ affect later stages. This is an issue in two specific cases.
   For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
   (from before the flag defaulted to `false`).
   
+To modify either of these flags both for building and editing the stdlib, adjust
+the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
+on the next `update-stage0` when the file is overwritten with the original
+version in `src/`.
+
 Development Setup
 -----------------
 

nix/bootstrap.nix

@@ -74,7 +74,6 @@ rec {
         src = ../src;
         fullSrc = ../.;
         inherit debug;
-        leanFlags = [ "-Dinterpreter.prefer_native=false" ];
       });
     in (all: all // all.lean) rec {
       Init = build { name = "Init"; deps = []; };

src/library/compiler/ir_interpreter.cpp

@@ -48,13 +48,8 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include "util/option_declarations.h"
 
 #ifndef LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE
-#if LEAN_IS_STAGE0 == 1
-// We already set `-Dinterpreter.prefer_native=false` in stdlib.make, but also set it here as a default when we use stage 0 in the editor
-#define LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE false
-#else
 #define LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE true
 #endif
-#endif
 
 namespace lean {
 namespace ir {

src/shell/lean.cpp

@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "initialize/init.h"
 #include "library/compiler/ir_interpreter.h"
 #include "util/path.h"
+#include "stdlib_flags.h"
 #ifdef _MSC_VER
 #include <io.h>
 #define STDOUT_FILENO 1
@@ -429,7 +430,7 @@ int main(int argc, char ** argv) {
         return 1;
     }
 
-    options opts;
+    options opts = get_default_options();
     optional<std::string> server_in;
     std::string native_output;
     optional<std::string> c_output;

src/stdlib.make.in

@@ -14,7 +14,7 @@ LEANMAKE_OPTS=\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
 	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
+	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
 	LEAN_AR="${CMAKE_AR}"\

src/stdlib_flags.h

@@ -0,0 +1,15 @@
+#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;
+}
+}