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

refactor: compile runtime/ into new static library leanrt

Browse source
This commit is contained in:
Sebastian Ullrich 2021-08-16 13:29:43 +02:00
parent 70e22910d7
commit b7d723c982
3 changed files with 22 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
CMakeLists.txt
View file

@ -57,8 +57,7 @@ ExternalProject_add(stage2
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage2
# reuse libleancpp.a, which doesn't change
CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS}
CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage1
@ -68,7 +67,7 @@ ExternalProject_add(stage3
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage3
CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS}
CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage2

25
src/CMakeLists.txt
View file

@ -273,14 +273,13 @@ find_package(PythonInterp)
include_directories(${CMAKE_BINARY_DIR}/include)
# libleancpp and the stdlib libraries are cyclically dependent. This works by default on macOS, which also doesn't like
# libleancpp and libLean are cyclically dependent. This works by default on macOS, which also doesn't like
# the linker flags necessary on other platforms.
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lleanrt")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js")
set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
else()
# `-pie` defaulting is not consistent on Linux distributions, so let's default to off
set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group")
endif()
@ -375,16 +374,22 @@ 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(LEANCPP)
if(${STAGE} GREATER 1)
# reuse C++ parts, which don't change
add_library(leanrt STATIC IMPORTED)
set_target_properties(leanrt PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a")
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")
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
add_dependencies(leanrt copy-leancpp)
add_dependencies(leancpp copy-leancpp)
else()
add_subdirectory(runtime)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:runtime>)
add_subdirectory(util)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:util>)
add_subdirectory(kernel)
@ -415,9 +420,9 @@ string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
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 ${LEANSHARED_LINKER_FLAGS}")
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}/lib/lean/libleanrt.a ${LEANSHARED_LINKER_FLAGS}")
else()
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${LEANSHARED_LINKER_FLAGS}")
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive -lleanrt ${LEANSHARED_LINKER_FLAGS}")
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--out-implib,${CMAKE_BINARY_DIR}/bin/libleanshared.dll.a")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -L$bindir")
@ -430,7 +435,7 @@ 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
DEPENDS leancpp leanrt
# 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

10
src/runtime/CMakeLists.txt
View file

@ -3,16 +3,16 @@ object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp)
add_library(runtime OBJECT ${RUNTIME_OBJS})
add_library(leanruntime ${RUNTIME_OBJS})
add_library(leanrt STATIC ${RUNTIME_OBJS})
if(LLVM)
string(REPLACE ";" " " RUNTIME_OBJS_STR "${RUNTIME_OBJS};lean_inlines.c")
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
add_custom_command(
OUTPUT libleanruntime.bc
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}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -I$<JOIN:$<TARGET_PROPERTY:leanruntime,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 libleanruntime.bc"
COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -I$<JOIN:$<TARGET_PROPERTY:leanruntime,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 libleanruntime.bc)
add_custom_target(runtime_bc DEPENDS libleanrt.bc)
endif()