From 984fec7387fb442996d8e5bee3546d56870b0e9c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 8 May 2020 15:19:32 +0200
Subject: [PATCH] refactor: move update-stage0 out of Makefile

---
 script/update-stage0 | 12 ++++++++++++
 src/CMakeLists.txt   |  5 ++---
 src/Makefile.in      | 14 +-------------
 3 files changed, 15 insertions(+), 16 deletions(-)
 create mode 100755 script/update-stage0

diff --git a/script/update-stage0 b/script/update-stage0
new file mode 100755
index 0000000000..348ddadb99
--- /dev/null
+++ b/script/update-stage0
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+rm -r stage0 || true
+mkdir -p stage0/
+c_files="$(cd src; find Init -name '*.lean' | sed s/.lean/.c/ | sort)"
+for f in $c_files; do mkdir -p $(dirname stage0/stdlib/$f); cp $OUT/temp/$f stage0/stdlib/$f; done
+# ensure deterministic ordering
+echo "add_library (stage0 OBJECT $c_files)" > stage0/stdlib/CMakeLists.txt
+# don't copy untracked crap
+git ls-files -z src | xargs -0 -I '{}' bash -c 'mkdir -p `dirname stage0/{}` && cp {} stage0/{}'
+git add stage0
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e2f06bee2e..990bdaf18b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -547,10 +547,9 @@ else()
 endif()
 
 add_custom_target(update-stage0
-  COMMAND make update-stage0 -f ${CMAKE_BINARY_DIR}/share/lean/Makefile
-    "OUT=${CMAKE_BINARY_DIR}/lib"
+  COMMAND cmake -E env OUT=${CMAKE_BINARY_DIR}/lib bash script/update-stage0
   DEPENDS leanstdlib
-  WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}")
+  WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/..")
 
 configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
 install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
diff --git a/src/Makefile.in b/src/Makefile.in
index 06597b4ba8..45042465a6 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -4,14 +4,11 @@
 SRCS = $(shell find Init -name '*.lean')
 DEPS = $(addprefix $(OUT)/temp/,$(SRCS:.lean=.depend))
 OPTS = @LEAN_EXTRA_MAKE_OPTS@
-STAGE0_DIR = ../stage0
 ifndef OUT
 $(error "`OUT` must be set (use cmake)")
 endif
 export LEAN_PATH=Init=$(OUT)/lean/Init
 OBJS = $(addprefix $(OUT)/lean/, $(SRCS:.lean=.olean))
-# ensure deterministic ordering
-CS_CORE=$(sort $(SRCS:.lean=.c))
 
 SHELL = /usr/bin/env bash -eo pipefail
 
@@ -51,15 +48,6 @@ $(OUT)/libleanstdlib.a: $(addprefix $(OUT)/temp/,$(SRCS:.lean=.o))
 	@rm -f $@
 	@ar rcs $@ $^
 
-update-stage0:
-	-rm -r $(STAGE0_DIR)
-	-mkdir -p $(STAGE0_DIR)/stdlib
-	for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done
-	echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/stdlib/CMakeLists.txt
-# don't copy untracked crap
-	git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}'
-	-git add $(STAGE0_DIR)
-
-.PRECIOUS: %.depend $(OUT)/temp/%.c
+.PRECIOUS: $(OUT)/temp/%.c
 
 include $(DEPS)