From eb72fba635e40d05b8bebe89e3effa550764400f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 20 Jul 2021 21:58:27 +0200 Subject: [PATCH] refactor: build C files using leanmake/leanc in stage 0 as well --- script/update-stage0 | 9 ---- src/CMakeLists.txt | 105 +++++++++++++++++++++---------------------- src/lean.mk.in | 7 ++- src/stdlib.make.in | 9 ++-- 4 files changed, 61 insertions(+), 69 deletions(-) diff --git a/script/update-stage0 b/script/update-stage0 index 5c24b22338..85fd7a8046 100755 --- a/script/update-stage0 +++ b/script/update-stage0 @@ -2,19 +2,10 @@ set -euo pipefail rm -r stage0 || true -mkdir -p stage0/stdlib/ -cat <> stage0/stdlib/CMakeLists.txt -set(CMAKE_C_COMPILER_LAUNCHER "env;LEAN_CXX=\${CMAKE_CXX_COMPILER_LAUNCHER} \${CMAKE_CXX_COMPILER}") -set(CMAKE_C_COMPILER "\${CMAKE_BINARY_DIR}/bin/leanc") -EOF for pkg in Init Std Lean; do # ensure deterministic ordering c_files="$pkg.c $(cd src; find $pkg -name '*.lean' | sed s/.lean/.c/ | LC_ALL=C sort | tr '\n' ' ')" for f in $c_files; do mkdir -p $(dirname stage0/stdlib/$f); cp ${CP_PARAMS:-} $CSRCS/$f stage0/stdlib/$f; done - cat <> stage0/stdlib/CMakeLists.txt -add_library ($pkg STATIC $c_files) -set_target_properties($pkg PROPERTIES ARCHIVE_OUTPUT_DIRECTORY "\${CMAKE_BINARY_DIR}/lib/lean") -EOF done # don't copy untracked crap git ls-files -z src | xargs -0 -I '{}' bash -c 'mkdir -p `dirname stage0/{}` && cp {} stage0/{}' diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1c972d8146..33b86c9c2a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -415,9 +415,6 @@ else() set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(initialize) set(LEAN_OBJS ${LEAN_OBJS} $) - if(${STAGE} EQUAL 0) - add_subdirectory(../stdlib stdlib) - endif() add_library(leancpp STATIC ${LEAN_OBJS}) set_target_properties(leancpp PROPERTIES @@ -427,68 +424,68 @@ endif() # 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") -# make stdlib using previous stage -if(PREV_STAGE) - # ...and Make doesn't like absolute Windows paths either - # (also looks nicer in the build log) - file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib) +# ...and Make doesn't like absolute Windows paths either +# (also looks nicer in the build log) +file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib) - string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) - # These are used in lean.mk and passed through by stdlib.make - set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") - - if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") - set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a") - else() - set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive") - if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--out-implib,${CMAKE_BINARY_DIR}/bin/libleanshared.dll.a") - endif() - endif() - - # Escape for `make`. Yes, twice. - string(REPLACE "$" "$$$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}") - configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make) - add_custom_target(make_stdlib ALL - WORKING_DIRECTORY ${LEAN_SOURCE_DIR} - # needed for linking `leanpkg` - DEPENDS leancpp - # 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. - # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage - COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make) - - add_library(Init STATIC IMPORTED) - set_target_properties(Init PROPERTIES - IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libInit.a) - add_dependencies(Init make_stdlib) - - add_library(Std STATIC IMPORTED) - set_target_properties(Std PROPERTIES - IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libStd.a) - add_dependencies(Std make_stdlib) - - add_library(Lean STATIC IMPORTED) - set_target_properties(Lean PROPERTIES - IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libLean.a) - add_dependencies(Lean make_stdlib) - - add_library(leanshared SHARED IMPORTED) - set_target_properties(leanshared PROPERTIES - IMPORTED_LOCATION ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}) - add_dependencies(leanshared make_stdlib) +string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) +# These are used in lean.mk and passed through by stdlib.make +set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a") +else() + set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive") if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - install(FILES ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} DESTINATION bin) - install(FILES ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}.a DESTINATION bin) + set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--out-implib,${CMAKE_BINARY_DIR}/bin/libleanshared.dll.a") endif() +endif() +# Escape for `make`. Yes, twice. +string(REPLACE "$" "$$$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}") +configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make) +add_custom_target(make_stdlib ALL + WORKING_DIRECTORY ${LEAN_SOURCE_DIR} + # needed for linking `leanpkg` + DEPENDS leancpp + # 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. + # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage + COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared $,MORE_LEANMAKE_OPTS=C_ONLY=1\ C_OUT=../stdlib/,Leanpkg> + VERBATIM) + +add_library(Init STATIC IMPORTED) +set_target_properties(Init PROPERTIES + IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libInit.a) +add_dependencies(Init make_stdlib) + +add_library(Std STATIC IMPORTED) +set_target_properties(Std PROPERTIES + IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libStd.a) +add_dependencies(Std make_stdlib) + +add_library(Lean STATIC IMPORTED) +set_target_properties(Lean PROPERTIES + IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libLean.a) +add_dependencies(Lean make_stdlib) + +add_library(leanshared SHARED IMPORTED) +set_target_properties(leanshared PROPERTIES + IMPORTED_LOCATION ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}) +add_dependencies(leanshared make_stdlib) + +if(PREV_STAGE) add_custom_target(update-stage0 COMMAND cmake -E env CSRCS=${CMAKE_BINARY_DIR}/lib/temp bash script/update-stage0 DEPENDS make_stdlib WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..") endif() +if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") + install(FILES ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} DESTINATION bin) + install(FILES ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}.a DESTINATION bin) +endif() + configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY) install(FILES "${CMAKE_BINARY_DIR}/bin/leanc" DESTINATION bin diff --git a/src/lean.mk.in b/src/lean.mk.in index 680e3989f9..92fd1f97a3 100644 --- a/src/lean.mk.in +++ b/src/lean.mk.in @@ -16,6 +16,7 @@ LEAN_AR = ar OUT = build OLEAN_OUT = $(OUT) TEMP_OUT = $(OUT)/temp +C_OUT = $(TEMP_OUT) BIN_OUT = $(OUT)/bin LIB_OUT = $(OUT)/lib BIN_NAME = $(PKG) @@ -61,10 +62,12 @@ endif # create the .c file atomically mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c" +ifndef C_ONLY $(TEMP_OUT)/%.c: $(OLEAN_OUT)/%.olean @ +endif -$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.c +$(TEMP_OUT)/%.o: $(C_OUT)/%.c ifdef CMAKE_LIKE_OUTPUT @echo "[ ] Building $<" endif @@ -94,4 +97,6 @@ clean: .PRECIOUS: $(TEMP_OUT)/%.c +ifndef C_ONLY include $(DEPS) +endif diff --git a/src/stdlib.make.in b/src/stdlib.make.in index eff033f2ad..e5776c395b 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -19,11 +19,10 @@ LEANMAKE_OPTS=\ LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\ LEAN_AR="${CMAKE_AR}"\ MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ - CMAKE_LIKE_OUTPUT=1 + CMAKE_LIKE_OUTPUT=1\ + $(MORE_LEANMAKE_OPTS) -.PHONY: all Init Std Lean leanshared Leanpkg - -all: Init Std Lean leanshared Leanpkg +.PHONY: Init Std Lean leanshared Leanpkg Init: # Use `+` to use the Make jobserver with `leanmake` for parallelized builds @@ -38,7 +37,7 @@ Lean: Init Std leanshared: Init Std Lean @mkdir -p "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" || true # can't use leanc here since it would try to link against leanshared - "$LEAN_CXX" -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} + ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} ${LEANC_GMP} -L${LIB}/lean Leanpkg: Init Std Lean leanshared +"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE}'