From 89d6c702734b060ecd6b009e91caf7de55bc5809 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 8 Oct 2021 17:27:13 +0200 Subject: [PATCH] fix: macOS build --- src/CMakeLists.txt | 12 ++++++++---- src/runtime/CMakeLists.txt | 5 ++--- src/stdlib.make.in | 2 +- stage0/src/CMakeLists.txt | 11 +++++++---- stage0/src/runtime/CMakeLists.txt | 5 ++--- stage0/src/stdlib.make.in | 2 +- 6 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 65cfaf77f5..2e8129e360 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -382,6 +382,14 @@ 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 +string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) +# These are used in lean.mk (and libleanrt) and passed through by stdlib.make +# They are not embedded into `leanc` since they are build profile/machine specific +string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}") +if(CMAKE_OSX_DEPLOYMENT_TARGET) + string(APPEND LEANC_OPTS " ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}") +endif() + if(${STAGE} GREATER 1) # reuse C++ parts, which don't change add_library(leanrt_initial-exec STATIC IMPORTED) @@ -426,10 +434,6 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin") # (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}} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT} ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}") - 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 ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") else() diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 2ad8fda1d8..1dd7cc2707 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -11,12 +11,11 @@ set_target_properties(leanrt_initial-exec PROPERTIES # but introduces a measurable overhead while accessing the thread-local variable `g_heap` when allocating and deallocating. Therefore we compile # the runtime again with the more restrictive `local-exec` and use it when linking Lean code statically, i.e. not against `leanshared`. string(REPLACE ";" " " RUNTIME_OBJS_STR "${RUNTIME_OBJS}") -string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) add_custom_command( OUTPUT ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a DEPENDS ${RUNTIME_OBJS} # compile each runtime file with the original compile flags plus `-ftls-model=local-exec` - COMMAND bash -ec "rm -rf runtmp2 || true; mkdir runtmp2; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_CXX_FLAGS} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT} ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET} -ftls-model=local-exec -I$, -I> \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -c -o runtmp2/$f.o; done; ar rcs ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a runtmp2/*.o" + COMMAND bash -ec "rm -rf runtmp2 || true; mkdir runtmp2; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${LEANC_OPTS} -ftls-model=local-exec -I$, -I> \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -c -o runtmp2/$f.o; done; ar rcs ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a runtmp2/*.o" VERBATIM) add_custom_target(leanrt ALL DEPENDS ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a) @@ -25,7 +24,7 @@ if(LLVM) OUTPUT libleanrt.bc DEPENDS ${RUNTIME_OBJS} lean_inlines.c # compile each runtime file with the original compile flags plus `-emit-llvm`, then `llvm-link` them together - COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR} lean_inlines.c; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -I$, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanrt.bc" + COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR} lean_inlines.c; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${LEANC_OPTS} -I$, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanrt.bc" VERBATIM) add_custom_target(runtime_bc DEPENDS libleanrt.bc) endif() diff --git a/src/stdlib.make.in b/src/stdlib.make.in index c5eacb6b89..eca2ba5bb7 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -51,7 +51,7 @@ Leanpkg: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL) @echo "[ ] Building $@" - "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} -o $@ + "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index 65cfaf77f5..018f96fb6f 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -382,6 +382,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 +string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) +# These are used in lean.mk (and libleanrt) and passed through by stdlib.make +string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}") +if(CMAKE_OSX_DEPLOYMENT_TARGET) + string(APPEND LEANC_OPTS " ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}") +endif() + if(${STAGE} GREATER 1) # reuse C++ parts, which don't change add_library(leanrt_initial-exec STATIC IMPORTED) @@ -426,10 +433,6 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin") # (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}} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT} ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}") - 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 ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") else() diff --git a/stage0/src/runtime/CMakeLists.txt b/stage0/src/runtime/CMakeLists.txt index 2ad8fda1d8..1dd7cc2707 100644 --- a/stage0/src/runtime/CMakeLists.txt +++ b/stage0/src/runtime/CMakeLists.txt @@ -11,12 +11,11 @@ set_target_properties(leanrt_initial-exec PROPERTIES # but introduces a measurable overhead while accessing the thread-local variable `g_heap` when allocating and deallocating. Therefore we compile # the runtime again with the more restrictive `local-exec` and use it when linking Lean code statically, i.e. not against `leanshared`. string(REPLACE ";" " " RUNTIME_OBJS_STR "${RUNTIME_OBJS}") -string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) add_custom_command( OUTPUT ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a DEPENDS ${RUNTIME_OBJS} # compile each runtime file with the original compile flags plus `-ftls-model=local-exec` - COMMAND bash -ec "rm -rf runtmp2 || true; mkdir runtmp2; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_CXX_FLAGS} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT} ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET} -ftls-model=local-exec -I$, -I> \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -c -o runtmp2/$f.o; done; ar rcs ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a runtmp2/*.o" + COMMAND bash -ec "rm -rf runtmp2 || true; mkdir runtmp2; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${LEANC_OPTS} -ftls-model=local-exec -I$, -I> \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -c -o runtmp2/$f.o; done; ar rcs ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a runtmp2/*.o" VERBATIM) add_custom_target(leanrt ALL DEPENDS ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a) @@ -25,7 +24,7 @@ if(LLVM) OUTPUT libleanrt.bc DEPENDS ${RUNTIME_OBJS} lean_inlines.c # compile each runtime file with the original compile flags plus `-emit-llvm`, then `llvm-link` them together - COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR} lean_inlines.c; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -I$, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanrt.bc" + COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR} lean_inlines.c; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${LEANC_OPTS} -I$, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanrt.bc" VERBATIM) add_custom_target(runtime_bc DEPENDS libleanrt.bc) endif() diff --git a/stage0/src/stdlib.make.in b/stage0/src/stdlib.make.in index c5eacb6b89..eca2ba5bb7 100644 --- a/stage0/src/stdlib.make.in +++ b/stage0/src/stdlib.make.in @@ -51,7 +51,7 @@ Leanpkg: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL) @echo "[ ] Building $@" - "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} -o $@ + "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}