chore: fix interactive use of stage 0

src/CMakeLists.txt

@@ -478,6 +478,11 @@ endif ()
 
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
+if (${STAGE} EQUAL 0)
+  set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 1")
+else()
+  set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 0")
+endif()
 configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h")
 install(DIRECTORY ${LEAN_BINARY_DIR}/include/lean DESTINATION include)
 configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)

src/Lean/Util/Path.lean

@@ -29,9 +29,13 @@ constant searchPathRef : IO.Ref SearchPath := arbitrary _
 def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath :=
 pure $ System.FilePath.splitSearchPath path ++ sp
 
+@[extern c inline "LEAN_IS_STAGE0"]
+constant isStage0 (u : Unit) : Bool := arbitrary _
+
 def getBuiltinSearchPath : IO SearchPath := do
 appDir ← IO.appDir;
-pure [appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean"]
+-- use stage1 stdlib with stage0 executable (which should never be distributed outside of the build directory)
+pure [appDir ++ pathSep ++ ".." ++ (if isStage0 () then pathSep ++ ".." ++ pathSep ++ "stage1" else "") ++ pathSep ++ "lib" ++ pathSep ++ "lean"]
 
 def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
 val ← IO.getEnv "LEAN_PATH";

src/config.h.in

@@ -10,3 +10,4 @@ Author: Leonardo de Moura
 @LEAN_COMPRESSED_OBJECT_HEADER@
 @LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC@
 @LEAN_CHECK_RC_OVERFLOW@
+@LEAN_IS_STAGE0@