From 617f17facbc4822ebdbe698b9bb26e5bcfee4383 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 3 Jul 2021 16:28:07 +0200 Subject: [PATCH] feat: reintroduce libleanshared, link lean & leanpkg against it --- .github/workflows/ci.yml | 4 ++-- src/CMakeLists.txt | 51 ++++++++++++++++++++++------------------ src/shared/init.cpp | 11 --------- src/shell/CMakeLists.txt | 12 ++-------- src/stdlib.make.in | 20 +++++++++++++--- 5 files changed, 49 insertions(+), 49 deletions(-) delete mode 100644 src/shared/init.cpp diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a64987f12b..99ad4a96c8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -115,14 +115,14 @@ jobs: - name: Patch run: | for f in lean leanpkg; do - patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage1/bin/$f + patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --set-rpath '${ORIGIN}/../lib/lean' build/stage1/bin/$f done if: matrix.name == 'Linux release' - name: Patch run: | for f in lean leanpkg; do for lib in $(otool -L build/stage1/bin/$f | tail -n +2 | cut -d' ' -f1); do - install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/$f + [[ $lib ~= *lean* ]] || install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/$f done done if: matrix.name == 'macOS' diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 39f1af90ae..9fcd35f6cf 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -139,8 +139,14 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(EXTRA_UTIL_LIBS ${EXTRA_UTIL_LIBS} -lpsapi) endif() set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=${LEAN_WIN_STACK_SIZE}") + # DLLs must go next to executables on Windows + set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin") +else() + set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean") endif() +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean") + # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory. if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin")) set(LEAN_EXTRA_MAKE_OPTS -s40000 ${LEAN_EXTRA_MAKE_OPTS}) @@ -190,7 +196,7 @@ endif() set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules") # Initialize CXXFLAGS. -set(CMAKE_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\"") +set(CMAKE_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -fPIC -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\"") set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG -DLEAN_TRACE") set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG") set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG") @@ -302,11 +308,8 @@ endif() # export all symbols for the interpreter if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -Wl,--export-all") - set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all") set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -Wl,--export-all") else() - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic") set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -ldl") set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -ldl") endif() @@ -317,12 +320,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -lbcrypt") endif() +set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,'-rpath=\${ORIGIN}/../lib/lean'") + + # Allow `lean` symbols in plugins without linking directly against it. If we linked against the # 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 - set(LEANC_SHARED_LINKER_FLAGS "$bindir/lean.exe.a") + # import library created by the `leanshared` target + set(LEANC_SHARED_LINKER_FLAGS "$bindir/leanshared.dll.a") elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") set(LEANC_SHARED_LINKER_FLAGS "-Wl,-undefined,dynamic_lookup") endif() @@ -407,10 +413,8 @@ else() add_library(leancpp STATIC ${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) # 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") @@ -425,6 +429,12 @@ if(PREV_STAGE) # 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") + endif() + configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make) add_custom_target(make_stdlib ALL WORKING_DIRECTORY ${LEAN_SOURCE_DIR} @@ -450,14 +460,22 @@ if(PREV_STAGE) 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(${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() + 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() -target_link_libraries(leancpp INTERFACE ${EXTRA_LIBS}) - configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY) install(FILES "${CMAKE_BINARY_DIR}/bin/leanc" DESTINATION bin @@ -470,19 +488,6 @@ install(FILES "${CMAKE_BINARY_DIR}/bin/leanpkg${CMAKE_EXECUTABLE_SUFFIX}" 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 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. -# if (NOT("${CROSS_COMPILE}" MATCHES "ON")) -# if ("${STATIC}" MATCHES "OFF") -# add_library(leanshared SHARED shared/init.cpp) -# # see `target_link_libraries(lean ...)` -# target_link_libraries(leanshared leancpp Init leancpp Init) -# install(TARGETS leanshared DESTINATION lib) -# endif() -# endif() - add_subdirectory(shell) add_custom_target(clean-stdlib diff --git a/src/shared/init.cpp b/src/shared/init.cpp deleted file mode 100644 index 98c325b8a7..0000000000 --- a/src/shared/init.cpp +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "initialize/init.h" -namespace lean { -// automatic initialization for the shared library -initializer g_init; -} diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index eb14a4a882..171f281d3c 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -25,9 +25,9 @@ endif() string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} - COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc $ ${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}" + COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc $ -lleanshared ${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}" VERBATIM - DEPENDS Init Std Lean leancpp shell $,runtime_bc,>) + DEPENDS leanshared shell $,runtime_bc,>) add_custom_target(lean ALL DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}) @@ -36,14 +36,6 @@ install(FILES ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} DESTINATION bin PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE) -# broken, will likely fix in the future by linking against shared libraries instead -## 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,${CMAKE_BINARY_DIR}/bin/lean.exe.a") -#endif() - # use executable of current stage for tests string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin") diff --git a/src/stdlib.make.in b/src/stdlib.make.in index acc59d2615..946ae2aca3 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -15,15 +15,29 @@ LEANMAKE_OPTS=\ OLEAN_OUT="${LIB}/lean"\ BIN_OUT="${CMAKE_BINARY_DIR}/bin"\ LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\ - LEANC_OPTS+="${LEANC_OPTS}"\ + LEANC_OPTS+="${LEANC_OPTS} -fPIC"\ 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 -stdlib: +.PHONY: all Init Std Lean leanshared Leanpkg + +all: Init Std Lean leanshared Leanpkg + +Init: # Use `+` to use the Make jobserver with `leanmake` for parallelized builds +"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS) + +Std: Init +"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS) + +Lean: Init Std +"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) - +"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS="${CMAKE_EXE_LINKER_FLAGS}" + +leanshared: Init Std Lean + @mkdir -p "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" || true + "${LEAN_BIN}/leanc" -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} + +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}"