refactor: move update-stage0 out of Makefile

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

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"

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)