From 402d4437c0c36d12de98c75bc83cb372f40c8d5c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 25 Sep 2020 11:08:48 +0200
Subject: [PATCH] chore: fix interactive use of stage 0

---
 src/CMakeLists.txt      | 5 +++++
 src/Lean/Util/Path.lean | 6 +++++-
 src/config.h.in         | 1 +
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f809d3e7b2..dad308e644 100644
--- a/src/CMakeLists.txt
+++ b/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)
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 87bf7d6951..2c65b642d8 100644
--- a/src/Lean/Util/Path.lean
+++ b/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";
diff --git a/src/config.h.in b/src/config.h.in
index d9f524afd8..0fec0771e5 100644
--- a/src/config.h.in
+++ b/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@