From beae045ebcb88d6c39d78183f3b207fadca86949 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 21 Mar 2019 10:12:56 +0100
Subject: [PATCH] fix(CMakeLists): complete move of stage1 from src/ to build
 dir

---
 doc/make/index.md        | 2 +-
 library/Makefile.in      | 2 +-
 src/CMakeLists.txt       | 4 ++--
 src/shell/CMakeLists.txt | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/make/index.md b/doc/make/index.md
index 2f73cf212d..42ff59cb33 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -83,7 +83,7 @@ building Lean itself - which is needed to again build those parts. Building the
   `.olean` object files as well as extracted to C++ in `src/stage1` by the
   target `stdlib`.
 * The target `build_libleanstdlib` builds the static library
-  `src/stage1/libleanstdlib.a` from the extracted files.
+  `stage1/libleanstdlib.a` from the extracted files.
 * This library is linked with the C++ source files into `libleanstatic.a` and
   ultimately into the executable `lean`.
 * The `bin` target finally copies the executable and libraries into `bin/`.
diff --git a/library/Makefile.in b/library/Makefile.in
index cd7c7433ae..6509ef2b78 100644
--- a/library/Makefile.in
+++ b/library/Makefile.in
@@ -32,7 +32,7 @@ depends: $(DEPS)
 clean:
 	find . -name *.olean -delete
 	find . -name *.depend -delete
-	[ -d $(STAGE1_DIR) ] && find $(STAGE1_DIR) -name *.cpp -delete
+	[ -d "$(STAGE1_DIR)" ] && rm -r "$(STAGE1_DIR)"
 
 $(STAGE1_DIR)/%.cpp: %.olean
 	@
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8d79d4ae36..861e1f2118 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -455,12 +455,12 @@ add_library(leanstatic_stage0 ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS} $<TARGET_OBJECTS
 target_link_libraries(leanstatic_stage0 ${EXTRA_LIBS})
 
 add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
-target_link_libraries(leanstatic "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a" ${EXTRA_LIBS})
+target_link_libraries(leanstatic "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" ${EXTRA_LIBS})
 add_dependencies(leanstatic stdlib)
 
 ADD_CUSTOM_TARGET(bin_lib ALL
    COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-   COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${LEAN_SOURCE_DIR}/stage1/libleanstdlib*" "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
+   COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${CMAKE_BINARY_DIR}/stage1/libleanstdlib*" "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
    DEPENDS leanstatic
 )
 # Configure leanc
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 1c024a5cb8..c0bb725188 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -8,7 +8,7 @@ endif()
 
 add_custom_target(stdlib
   # '-G Ninja' complains otherwise
-  BYPRODUCTS "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a"
+  BYPRODUCTS "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
   WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
   COMMAND make -j8 "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$<TARGET_FILE:lean_stage0>" "STAGE1_DIR=${CMAKE_BINARY_DIR}/stage1"
   DEPENDS lean_stage0)