chore: add stage 1.5 (yes, really)

CMakeLists.txt

@@ -44,6 +44,16 @@ ExternalProject_add(stage1
   DEPENDS stage0 stage0.5
   EXCLUDE_FROM_ALL ON
 )
+ExternalProject_add(stage1.5
+  SOURCE_DIR "${LEAN_SOURCE_DIR}"
+  SOURCE_SUBDIR src
+  BINARY_DIR stage1.5
+  CMAKE_ARGS -DSTAGE=1.5 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
+  BUILD_ALWAYS ON
+  INSTALL_COMMAND ""
+  DEPENDS stage1
+  EXCLUDE_FROM_ALL ON
+)
 ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src

doc/make/index.md

@@ -116,8 +116,11 @@ programs. In fact, if the stage 0 library and the stage 1 are compatible (use th
 same Lean ABI, so to speak), we can avoid even rebuilding the stage 1 library
 using a special stage "0.5" that combines the stage 1 compiler with the stage 0
 library. Most changes do not break this ABI, so running `make` by itself in the
-root build folder will default to `make stage0.5`. In summary, doing a standard
-build via `make` involves these steps:
+root build folder will default to `make stage0.5`. There is also an analogous
+stage 1.5, which should be sufficient for testing changes to *meta*programs on
+the stdlib.
+
+In summary, doing a standard build via `make` involves these steps:
 
 1. compile the `stage0/src` archived sources into `stage0/bin/lean`
 1. use it to compile the library (*including* your changes) into `stage0/lib`

src/stdlib.make.in

@@ -10,8 +10,8 @@ LEANMAKE_OPTS=\
 	CMAKE_LIKE_OUTPUT=1
 
 stdlib:
-ifeq "${STAGE}" "0.5"
-# In the case of stage 0.5, we simply hardlink .olean files and libInit.a from stage 0 (but not libleancpp.a,
+ifeq ($(patsubst %.5,.5,${STAGE}), .5)
+# In the case of stage n.5, we simply copy .olean files and libInit.a from stage n (but not libleancpp.a,
 # which is different from stage 0).
 	mkdir -p "${LIB}/lean"
 	cp -rf $$(find "${PREV_STAGE}/lib/lean" -mindepth 1 -maxdepth 1 -not -name libleancpp.a) "${LIB}/lean"