refactor: make stages internally consistent by compiling the stageN lib with the stageN compiler, rename static libraries

The old stage1 is now stage0.5, which at least suggests that it's not an entirely consistent stage in general

.github/workflows/ci.yml

@@ -26,8 +26,6 @@ jobs:
             CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
           - name: Linux fsanitize
             os: ubuntu-latest
-            # do one sanitized build of the stdlib
-            build-stage2: true
             # turn off custom allocator to make LSAN do its magic
             CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
           - name: Linux LLVM=ON
@@ -87,10 +85,10 @@ jobs:
         run: msys2do ./script/ci.sh
         if: matrix.os == 'windows-latest'
       - name: Test
-        run: nix-shell --run "cd build; ctest -j4 --output-on-failure < /dev/null"
+        run: nix-shell --run "cd build/stage0.5; ctest -j4 --output-on-failure < /dev/null"
         if: matrix.os != 'windows-latest'
       - name: Test
-        run: msys2do cd build; ctest -j4 --output-on-failure ^< /dev/null
+        run: msys2do cd build/stage0.5; ctest -j4 --output-on-failure ^< /dev/null
         shell: cmd
         if: matrix.os == 'windows-latest'
       - name: Build Stage 2
@@ -100,7 +98,7 @@ jobs:
         run: nix-shell --run "cd build; make -j4 check-stage3"
         if: matrix.check-stage3
       - name: Test Speedcenter Benchmarks
-        run: PATH=$(realpath build/stage1/bin):$PATH nix-shell --run 'cd tests/bench; temci exec --config speedcenter.yaml --runs 1'
+        run: PATH=$(realpath build/stage0.5/bin):$PATH nix-shell --run 'cd tests/bench; temci exec --config speedcenter.yaml --runs 1'
         if: matrix.test-speedcenter
       - name: CCache stats
         run: nix-shell --run "ccache -s"

CMakeLists.txt

@@ -12,31 +12,43 @@ endforeach()
 
 include(ExternalProject)
 project(LEAN CXX C)
+# use the same library sources everywhere; this only important for stage 0 since the compiler source for it come from stage0/src
+list(APPEND CL_ARGS "-DLIB_SOURCE_DIR=${LEAN_SOURCE_DIR}/src")
 
 ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
   SOURCE_SUBDIR src
   BINARY_DIR stage0
   # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=0 ${CL_ARGS} -DUSE_GITHASH=OFF
   BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
   INSTALL_COMMAND ""  # skip install
 )
+ExternalProject_add(stage0.5
+  SOURCE_DIR "${LEAN_SOURCE_DIR}"
+  SOURCE_SUBDIR src
+  BINARY_DIR stage0.5
+  CMAKE_ARGS -DSTAGE=0.5 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS}
+  BUILD_ALWAYS ON
+  INSTALL_COMMAND ""
+  DEPENDS stage0
+)
 ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS}
+  # reuse libleancpp.a, which doesn't change
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS stage0
+  DEPENDS stage0 stage0.5
+  EXCLUDE_FROM_ALL ON
 )
 ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  # reuse libleanstatic.a, which doesn't change
-  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANSTATIC="${CMAKE_BINARY_DIR}/stage1/lib/libleanstatic.a" ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=2 -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
@@ -46,7 +58,9 @@ ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANSTATIC="${CMAKE_BINARY_DIR}/stage1/lib/libleanstatic.a" ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
+  # skip building library - if `lean` is the same as in stage2, the library will be as well
+  BUILD_COMMAND $(MAKE) lean
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2

script/ci.sh

@@ -4,4 +4,4 @@ mkdir build
 cd build
 eval cmake .. $CMAKE_OPTIONS
 make
-(cd stage1; cpack)
+(cd stage0.5; cpack)

script/update-stage0

@@ -3,8 +3,8 @@ 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
+c_files="$(cd src; find Init -name '*.lean' | sed s/.lean/.c/ | sort | tr '\n' ' ')"
+for f in $c_files; do mkdir -p $(dirname stage0/stdlib/$f); cp $LIB/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

src/CMakeLists.txt

@@ -5,7 +5,9 @@ endif()
 if(NOT (${CMAKE_GENERATOR} MATCHES "Unix Makefiles"))
   message(FATAL_ERROR "The only supported CMake generator at the moment is 'Unix Makefiles'")
 endif()
-include(ExternalProject)
+if(NOT (DEFINED STAGE))
+  message(FATAL_ERROR "STAGE must be set; use the CMakeLists.txt in the root folder")
+endif()
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 0)
@@ -440,8 +442,8 @@ endif()
 # executable or `leanshared`, plugins would try to look them up at load time (even though they
 # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  # import library created by the `lean` target (and copied by `bin_lean`)
-  set(LEANC_SHARED_LINKER_FLAGS "$bindir/liblean.dll.a")
+  # import library created by the `lean` target
+  set(LEANC_SHARED_LINKER_FLAGS "$bindir/lean.exe.a")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
   set(LEANC_SHARED_LINKER_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,-undefined,dynamic_lookup")
 endif()
@@ -498,14 +500,13 @@ include_directories(${LEAN_SOURCE_DIR})
 include_directories(${CMAKE_BINARY_DIR})  # version.h etc., "private" headers
 include_directories(${CMAKE_BINARY_DIR}/include)  # config.h etc., "public" headers
 
-if(LEANSTATIC)
-  add_library(leanstatic STATIC IMPORTED)
-  set_target_properties(leanstatic PROPERTIES
-    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/libleanstatic.a")
-  target_link_libraries(leanstatic INTERFACE ${EXTRA_LIBS})
-  add_custom_target(copy-leanstatic
-    COMMAND cmake -E copy_if_different "${LEANSTATIC}" "${CMAKE_BINARY_DIR}/lib/libleanstatic.a")
-  add_dependencies(leanstatic copy-leanstatic)
+if(LEANCPP)
+  add_library(leancpp STATIC IMPORTED)
+  set_target_properties(leancpp PROPERTIES
+    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
+  add_custom_target(copy-leancpp
+    COMMAND cmake -E copy_if_different "${LEANCPP}" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
+  add_dependencies(leancpp copy-leancpp)
 else()
   add_subdirectory(runtime)
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:runtime>)
@@ -531,25 +532,33 @@ else()
     add_subdirectory(../stdlib stdlib)
   endif()
 
-  add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
-  set_target_properties(leanstatic PROPERTIES ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib")
-  target_link_libraries(leanstatic ${EXTRA_LIBS})
-endif()
-
-if(LLVM)
-  target_link_libraries(leanstatic ${llvm_libs})
+  add_library(leancpp ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
+  set_target_properties(leancpp PROPERTIES
+    ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean"
+    OUTPUT_NAME leancpp)
 endif()
+install(FILES ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a DESTINATION lib/lean)
 
 if(${STAGE} EQUAL 0)
-  add_library(leanstdlib STATIC $<TARGET_OBJECTS:stage0>)
+  add_library(Init STATIC $<TARGET_OBJECTS:stage0>)
 else()
-  add_library(leanstdlib STATIC IMPORTED)
+# created by the previous stage
+  add_library(Init STATIC IMPORTED)
+  set_target_properties(Init PROPERTIES
+    IMPORTED_LOCATION "${PREV_STAGE}/lib/lean/libInit.a")
+endif()
+# leancpp and Init are cyclically dependent
+target_link_libraries(Init INTERFACE leancpp)
+target_link_libraries(leancpp INTERFACE Init ${EXTRA_LIBS})
+
+if(LLVM)
+  target_link_libraries(leancpp INTERFACE ${llvm_libs})
 endif()
 
 add_custom_target(update-stage0
-  COMMAND cmake -E env OUT=${CMAKE_BINARY_DIR}/lib bash script/update-stage0
-  DEPENDS leanstdlib
-  WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/..")
+  COMMAND cmake -E env LIB=${CMAKE_BINARY_DIR}/lib bash script/update-stage0
+  DEPENDS Init
+  WORKING_DIRECTORY "${LIB_SOURCE_DIR}/..")
 
 configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
 install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
@@ -560,7 +569,7 @@ install(FILES ${LEAN_SOURCE_DIR}/bin/leanmake
   DESTINATION bin
   PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
 
-# shared library deactivated until we figure out the leanstatic/leanstdlib story
+# shared library deactivated until we figure out the leancpp/Init story
 # # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
 # # For some strange reason, it contains a copy of pthread_equal.
 # # Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
@@ -568,10 +577,9 @@ install(FILES ${LEAN_SOURCE_DIR}/bin/leanmake
 #   if ("${STATIC}" MATCHES "OFF")
 #     add_library(leanshared SHARED shared/init.cpp)
 #     # see `target_link_libraries(lean ...)`
-#     target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
+#     target_link_libraries(leanshared leancpp Init leancpp Init)
 #     install(TARGETS leanshared DESTINATION lib)
 #   endif()
-#   install(TARGETS leanstatic DESTINATION lib)
 # endif()
 
 add_subdirectory(shell)
@@ -618,9 +626,7 @@ add_custom_target(clean-stdlib
 add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
-install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean" DESTINATION "${LIBRARY_DIR}"
-        FILES_MATCHING
-        PATTERN "*.olean")
+install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean" DESTINATION "${LIBRARY_DIR}")
 
 install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean"
         FILES_MATCHING

src/Makefile.in

@@ -18,12 +18,14 @@ OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean))
 
 SHELL = /usr/bin/env bash -eo pipefail
 
-.PHONY: all bin depends
+.PHONY: all bin lib depends
 
 all: $(OBJS)
 
 bin: $(BIN_OUT)/$(PKG)
 
+lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
+
 depends: $(DEPS)
 
 # `lean --deps` complains if the `LEAN_PATH` doesn't point at anything

src/bin/leanc.in

@@ -12,8 +12,8 @@
 set -e
 bindir=$(dirname $0)
 
-# NOTE: leanstatic and leanstdlib are cyclically dependent
-linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib"
+# NOTE: libleancpp and libInit are cyclically dependent
+linker_flags="-lleancpp -lInit -lleancpp -lInit"
 for arg in "$@"; do
     [[ $arg == "-shared" ]] && linker_flags="@LEANC_SHARED_LINKER_FLAGS@"
 done
@@ -27,4 +27,4 @@ done
 [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
 
 # Note the `-x c` for treating all input as C code
-@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -x c -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
+@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" -x c "$@" -x none "-L$bindir/../lib/lean" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument

src/bin/leanmake

@@ -2,4 +2,4 @@
 
 set -euo pipefail
 bindir=$(dirname $0)
-make -f "$bindir/../share/lean/Makefile" "$@"
+PATH="$bindir:$PATH" ${MAKE:-make} -f "$bindir/../share/lean/Makefile" "$@"

src/shell/CMakeLists.txt

@@ -1,50 +1,33 @@
-if(PREV_STAGE)
-  string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
-  set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
-
-  # MSYS2 bash usually handles absolute Windows paths relatively well, but not when putting them in the PATH
-  file(RELATIVE_PATH PREV_STAGE_REL ${LEAN_SOURCE_DIR} ${PREV_STAGE})
-  # ...and Make doesn't like absolute Windows paths either
-  file(RELATIVE_PATH OUT ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
-
-  add_custom_target(make_stdlib
-    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
-    # fun: we use `bash -c` to set the `PATH`, but then pass other arguments outside so we don't have to escape them
-    COMMAND bash -c 'PATH=${PREV_STAGE_REL}/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile ${OUT}/libleanstdlib.a \"$$@\"'
-      # `$0`, ignored by `$@`
-      bash
-      PKG=Init
-      OUT=${OUT}
-      OLEAN_OUT=${OUT}/lean
-      LIB_OUT=${OUT}
-      STATIC_LIB_NAME=libleanstdlib.a
-      LEANC_OPTS=${LEANC_OPTS}
-      # recreate everything if the previous compiler has changed
-      MORE_DEPS=${PREV_STAGE_REL}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})
-  set_target_properties(leanstdlib PROPERTIES
-    IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/libleanstdlib.a"
-    IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
-  add_dependencies(leanstdlib make_stdlib)
-  install(FILES "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
-endif()
-
 add_executable(lean lean.cpp)
 set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
-
-# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
-# We use the approach described at
-# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
-# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
-target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
+target_link_libraries(lean leancpp Init)
 
 # create import library on Windows to link plugins against
 set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # https://github.com/msys2/MINGW-packages/issues/5952
-  target_link_options(lean PRIVATE "-Wl,--out-implib,$<TARGET_LINKER_FILE:lean>")
+  target_link_options(lean PRIVATE "-Wl,--out-implib,${CMAKE_BINARY_DIR}/bin/lean.exe.a")
 endif()
 install(TARGETS lean DESTINATION bin)
 
+string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
+set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
+
+# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
+string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
+# ...and Make doesn't like absolute Windows paths either
+# (also looks nicer in the build log)
+file(RELATIVE_PATH LIB ${LIB_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
+
+configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
+add_custom_target(make_stdlib ALL
+  WORKING_DIRECTORY ${LIB_SOURCE_DIR}
+  # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
+  # for a parallelized nested build, but CMake doesn't let us do that.
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make
+  DEPENDS lean)
+install(FILES ${CMAKE_BINARY_DIR}/lib/lean/libInit.a DESTINATION lib)
+
 # add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_BINARY_DIR}/bin/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
 # add_test(lean_export ${CMAKE_BINARY_DIR}/bin/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
 add_test(lean_help1    "${CMAKE_BINARY_DIR}/bin/lean" --help)
@@ -59,9 +42,6 @@ add_test(lean_ghash2   "${CMAKE_BINARY_DIR}/bin/lean" --githash)
 add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z")
 add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean")
 
-# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
-string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
-
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
 FOREACH(T ${LEANTESTS})

src/stdlib.make.in

@@ -0,0 +1,20 @@
+SHELL := /usr/bin/env bash
+
+stdlib:
+# (I don't know how to add comments inside a multiline rule, so all comments go first)
+# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
+# In the case of stage 0.5, we simply hardlink .olean files and libInit.a from stage 0 (but not libleancpp.a,
+# which is different from stage 0).
+# Otherwise, we build the library with `leanmake`. We rebuild it (`MORE_DEPS`) whenever the compiler has changed.
+	+if [ ${STAGE} == 0.5 ]; then\
+    mkdir -p "${LIB}/lean";\
+    cp -rlf $$(find "${PREV_STAGE}/lib/lean" -mindepth 1 -maxdepth 1 -not -name libleancpp.a) "${LIB}/lean";\
+  else\
+    "${LEAN_BIN}/leanmake" lib\
+      PKG=Init\
+      "OUT=${LIB}"\
+      "LIB_OUT=${LIB}/lean"\
+      "OLEAN_OUT=${LIB}/lean"\
+      "LEANC_OPTS=${LEANC_OPTS}"\
+      "MORE_DEPS=${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}";\
+  fi