max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: macOS build

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-08 17:27:13 +02:00
parent c8b998a607
commit 89d6c70273
6 changed files with 21 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/CMakeLists.txt
View file

@ -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()

5
src/runtime/CMakeLists.txt
View file

@ -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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()

2
src/stdlib.make.in
View file

@ -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}

11
stage0/src/CMakeLists.txt generated
View file

@ -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()

5
stage0/src/runtime/CMakeLists.txt generated
View file

@ -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -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()

2
stage0/src/stdlib.make.in generated
View file

@ -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}