From ccbc9d00dba92293656d4693192c6acd81c9b1ab Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 20 Aug 2021 15:37:16 +0200 Subject: [PATCH] Revert "feat: reintroduce libleanshared, link lean & leanpkg against it" --- .github/workflows/ci.yml | 28 ++- CMakeLists.txt | 5 +- doc/make/msys2.md | 2 +- flake.nix | 2 +- nix/bootstrap.nix | 29 +-- nix/buildLeanPackage.nix | 16 +- script/update-stage0 | 9 + shell.nix | 2 +- src/CMakeLists.txt | 221 ++++++++++++----------- src/bin/leanc.in | 4 +- src/initialize/init.cpp | 2 - src/lean.mk.in | 9 +- src/library/compiler/ir_interpreter.cpp | 12 +- src/runtime/CMakeLists.txt | 26 +-- src/shared/init.cpp | 11 ++ src/shell/CMakeLists.txt | 43 +++-- src/stdlib.make.in | 22 +-- tests/bench/speedcenter.exec.velcom.yaml | 4 +- 18 files changed, 217 insertions(+), 230 deletions(-) create mode 100644 src/shared/init.cpp diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ad1b0f2524..a64987f12b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,6 +26,7 @@ jobs: - name: Linux release os: ubuntu-latest release: true + CMAKE_OPTIONS: -DSTATIC=ON shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" - name: Linux os: ubuntu-latest @@ -36,16 +37,17 @@ jobs: CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug - name: Linux fsanitize os: ubuntu-latest - # turn off custom allocator & symbolic functions to make LSAN do its magic - CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC_FUNCTIONS=OFF + # turn off custom allocator to make LSAN do its magic + CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF - name: macOS os: macos-latest release: true + CMAKE_OPTIONS: -DSTATIC=ON - name: Windows os: windows-latest release: true shell: msys2 {0} - CMAKE_OPTIONS: -G "Unix Makefiles" + CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTATIC=ON # complete all jobs fail-fast: false name: ${{ matrix.name }} @@ -70,7 +72,7 @@ jobs: - name: Install MSYS2 uses: msys2/setup-msys2@v2 with: - install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc mingw-w64-x86_64-ccache git diffutils + install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git diffutils if: matrix.os == 'windows-latest' - name: Cache uses: actions/cache@v2 @@ -106,40 +108,34 @@ jobs: fi cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS make -j4 + - name: Lean stats + run: | + build/stage1/bin/lean --stats src/Lean.lean # de-Nix-ify binaries - name: Patch run: | for f in lean leanpkg; do - patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --set-rpath '${ORIGIN}/../lib:${ORIGIN}/../lib/lean' build/stage1/bin/$f + patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage1/bin/$f done if: matrix.name == 'Linux release' - name: Patch run: | for f in lean leanpkg; do - otool -L build/stage1/bin/$f for lib in $(otool -L build/stage1/bin/$f | tail -n +2 | cut -d' ' -f1); do - [[ "$lib" == *lean* ]] || install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/$f + 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' - - name: Test Binary without Nix Shell - shell: bash {0} - run: | - build/stage1/bin/lean -h - if: matrix.name != 'Windows' - name: Pack run: cd build/stage1; cpack - uses: actions/upload-artifact@v2 with: name: build-${{ matrix.name }} path: build/stage1/lean-* - - name: Lean stats - run: | - build/stage1/bin/lean --stats src/Lean.lean - name: Test run: | cd build/stage1 - ctest -j4 --output-on-failure --timeout 300 < /dev/null + ctest -j4 --output-on-failure < /dev/null - name: Build Stage 2 run: | cd build diff --git a/CMakeLists.txt b/CMakeLists.txt index 54deea01e6..065692e1f8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -57,7 +57,8 @@ ExternalProject_add(stage2 SOURCE_DIR "${LEAN_SOURCE_DIR}" SOURCE_SUBDIR src BINARY_DIR stage2 - CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 ${CL_ARGS} + # 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} BUILD_ALWAYS ON INSTALL_COMMAND "" DEPENDS stage1 @@ -67,7 +68,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 ${CL_ARGS} + CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS} BUILD_ALWAYS ON INSTALL_COMMAND "" DEPENDS stage2 diff --git a/doc/make/msys2.md b/doc/make/msys2.md index b1727b05eb..4f30fc05f6 100644 --- a/doc/make/msys2.md +++ b/doc/make/msys2.md @@ -19,7 +19,7 @@ MSYS2 has a package management system, [pacman][pacman], which is used in Arch L Here are the commands to install all dependencies needed to compile Lean on your machine. ```bash -pacman -S make mingw-w64-x86_64-cmake mingw-w64-x86_64-ccache mingw-w64-x86_64-gcc git +pacman -S make mingw-w64-x86_64-cmake mingw-w64-x86_64-ccache mingw-w64-x86_64-clang git ``` Then follow the [generic build instructions](index.md) in the MSYS2 MinGW shell, using diff --git a/flake.nix b/flake.nix index fe5ca13ced..861bdefa60 100644 --- a/flake.nix +++ b/flake.nix @@ -34,7 +34,7 @@ packages = lean-packages // rec { debug = lean-packages.override { debug = true; }; stage0debug = lean-packages.override { stage0debug = true; }; - sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC_FUNCTIONS=OFF" ]; }; + sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; }; sandebug = sanitized.override { debug = true; }; tsan = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ]; diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index eba2112103..9eeea9fc49 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -36,12 +36,11 @@ rec { leancpp = buildCMake { name = "leancpp"; src = ../src; - buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ]; + buildFlags = [ "leancpp" "shell" ]; installPhase = '' mkdir -p $out mv lib/ $out/ mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib - mv runtime/libleanrt_initial-exec.a $out/lib ''; }; # rename derivation so `nix run` uses the right executable name but we still see the stage in the build log @@ -77,34 +76,24 @@ rec { inherit debug; }); in (all: all // all.lean) rec { - inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package; Init = build { name = "Init"; deps = []; }; Std = build { name = "Std"; deps = [ Init ]; }; - Lean = build { name = "Lean"; deps = [ Init Std ]; }; - Leanpkg = build { name = "Leanpkg"; deps = [ Init Std Lean ]; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; }; - stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean"; - leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; } '' - mkdir $out - LEAN_CXX=${stdenv.cc}/bin/c++ ${lean-bin-tools-unwrapped}/bin/leanc -x none -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic-functions"} \ - ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a" - else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive"} ${stdlibLinkFlags} \ - -o $out/libleanshared${stdenv.hostPlatform.extensions.sharedLibrary} - ''; + Lean = build { name = "Lean"; deps = [ Init Std ]; linkFlags = ["${stdlibLinkFlags} -rdynamic ${leancpp}/lib/lean.cpp.o"]; }; + Leanpkg = build { name = "Leanpkg"; deps = [ Init Std Lean ]; linkFlags = ["${stdlibLinkFlags} -rdynamic"]; }; + inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package; mods = Init.mods // Std.mods // Lean.mods; + stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean"; leanc = writeShellScriptBin "leanc" '' - LEAN_CXX=${stdenv.cc}/bin/c++ ${lean-bin-tools-unwrapped}/bin/leanc ${stdlibLinkFlags} -L${leanshared} "$@" + LEAN_CXX=${stdenv.cc}/bin/c++ ${lean-bin-tools-unwrapped}/bin/leanc ${stdlibLinkFlags} "$@" ''; - lean = runCommand "lean" {} '' - mkdir -p $out/bin - ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean - ''; - leanpkg = Leanpkg.executable.withSharedStdlib; + lean = Lean.executable; + leanpkg = Leanpkg.executable; # derivation following the directory layout of the "basic" setup, mostly useful for running tests lean-all = wrapStage(stdenv.mkDerivation { name = "lean-${desc}"; buildCommand = '' mkdir -p $out/bin $out/lib/lean - ln -sf ${leancpp}/lib/lean/* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/ + ln -sf ${leancpp}/lib/lean/libleancpp.* ${Leanpkg.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* ${Init.staticLib}/* ${Init.modRoot}/* $out/lib/lean/ # put everything in a single final derivation so `IO.appDir` references work cp ${lean}/bin/lean ${leanpkg}/bin/leanpkg $out/bin # NOTE: first `bin/leanc` wins in case of `lndir` diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index f1296663a5..2442600c8d 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -2,7 +2,6 @@ stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, substituteAll, symlinkJoin, linkFarmFromDrvs, runCommand, ... }: let lean-final' = lean-final; in -lib.makeOverridable ( { name, src, fullSrc ? src, # Lean dependencies. Each entry should be an output of buildLeanPackage. deps ? [ lean.Lean lean.Leanpkg ], @@ -155,19 +154,12 @@ in rec { ${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)} \ -o $out/${name}.so ''; - executable = runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } '' + executable = runCommand executableName { buildInputs = [ stdenv.cc ]; } '' mkdir -p $out/bin - leanc -x none ${staticLib}/* ${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)} \ + ${leanc}/bin/leanc -x none ${staticLib}/* ${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)} \ -o $out/bin/${executableName} \ ${lib.concatStringsSep " " linkFlags} - '' // { - withSharedStdlib = runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } '' - mkdir -p $out/bin - leanc -x none ${staticLib}/* -lleanshared \ - -o $out/bin/${executableName} \ - ${lib.concatStringsSep " " linkFlags} - ''; - }; + ''; lean-package = writeShellScriptBin "lean" '' LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=${src}:$LEAN_SRC_PATH ${lean-final}/bin/lean "$@" @@ -197,4 +189,4 @@ in rec { lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev leanpkg-dev ]; }; emacs-dev = makeEmacsWrapper "emacs-dev" lean-dev; vscode-dev = makeVSCodeWrapper "vscode-dev" lean-dev; -}) +} diff --git a/script/update-stage0 b/script/update-stage0 index 85fd7a8046..5c24b22338 100755 --- a/script/update-stage0 +++ b/script/update-stage0 @@ -2,10 +2,19 @@ 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/shell.nix b/shell.nix index 470d6a82ce..344e5242df 100644 --- a/shell.nix +++ b/shell.nix @@ -8,7 +8,7 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: then flakePkgs.llvmPackages else pkgs.${"llvmPackages_${llvmPackages}"}).clang; } rec { - buildInputs = with pkgs; [ cmake gmp ccache ]; + buildInputs = with pkgs; [ cmake (gmp.override { withStatic = true; }) ccache ]; # https://github.com/NixOS/nixpkgs/issues/60919 hardeningDisable = [ "all" ]; # more convenient `ctest` output diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 44c84eaa72..39f1af90ae 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -31,6 +31,7 @@ enable_testing() option(MULTI_THREAD "MULTI_THREAD" ON) option(CCACHE "use ccache" ON) +option(STATIC "STATIC" OFF) option(SPLIT_STACK "SPLIT_STACK" OFF) # When OFF we disable LLVM support option(LLVM "LLVM" OFF) @@ -59,7 +60,6 @@ option(FAKE_FREE "Disable actually freeing runtime objects, useful for option(SMALL_ALLOCATOR "SMALL_ALLOCATOR" ON) option(LAZY_RC "LAZY_RC" OFF) option(RUNTIME_STATS "RUNTIME_STATS" OFF) -option(BSYMBOLIC_FUNCTIONS "Link with -Bsymbolic-functions to reduce call overhead in shared libraries (Linux)" ON) # development-specific options option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" ON) @@ -139,14 +139,8 @@ 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}) @@ -179,6 +173,19 @@ else() #message(WARNING "Disabling LLVM support. JIT compilation will not be available") endif() +if(STATIC) + # Creating a fully static executable is a bad idea in general when linking against libc and specifically + # with our dlopen shenanigans + message(STATUS "Linking libraries statically where possible") + if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") + set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static-libgcc -static-libstdc++") + endif() + set(CMAKE_FIND_LIBRARY_SUFFIXES ".a") + if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Windows") + set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,-Bstatic,--whole-archive -lwinpthread -Wl,--no-whole-archive,-Bdynamic") + endif() +endif() + # Set Module Path set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules") @@ -215,6 +222,7 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") endif () elseif (MSVC) # All good. Maybe enforce a recent version? + set(STATIC ON) # FIXME: not working yet set(CMAKE_CXX_FLAGS "/GL /EHsc /W2 /Zc:implicitNoexcept- -D_SCL_SECURE_NO_WARNINGS ${CMAKE_CXX_FLAGS}") set(CMAKE_CXX_FLAGS_DEBUG "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}") set(CMAKE_CXX_FLAGS_MINSIZEREL "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}") @@ -253,6 +261,7 @@ else() # GMP find_package(GMP 5.0.5 REQUIRED) include_directories(${GMP_INCLUDE_DIR}) + set(COPY_LIBS ${COPY_LIBS} ${GMP_LIBRARIES}) # dlopen set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS}) endif() @@ -268,62 +277,54 @@ if(CCACHE) endif() endif() +# TODO: copy COPY_LIBS when lean libraries become shared rather than static +set(EXTRA_LIBS ${EXTRA_LIBS} ${COPY_LIBS}) + # Python find_package(PythonInterp) include_directories(${CMAKE_BINARY_DIR}/include) -# libleancpp/Lean as well as libleanrt/Init/Std are cyclically dependent. This works by default on macOS, which also doesn't like +# libleancpp and the stdlib libraries 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 -lleanrt") + set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") - set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt") + set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js") else() - set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group") + # `-pie` defaulting is not consistent on Linux distributions, so let's default to off + set(LEANC_STATIC_LINKER_FLAGS "-no-pie -Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - if(BSYMBOLIC_FUNCTIONS) - set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -Wl,-Bsymbolic-functions") - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,-Bsymbolic-functions") - endif() - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC -ftls-model=initial-exec") - set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -fPIC") - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") -elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -ftls-model=initial-exec") - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-rpath,@executable_path/../lib:@executable_path/../lib/lean") + set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -fPIC") endif() # export all symbols for the interpreter if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - # for libraries compiled with `leanc -shared` + 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") - # for `leanshared` itself - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--export-all") - # for executables containing code to be interpreted - set(LEAN_DYN_EXE_LINKER_FLAGS "${LEAN_DYN_EXE_LINKER_FLAGS} -Wl,--export-all") else() - set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_LINKER_FLAGS} -ldl") - set(LEAN_DYN_EXE_LINKER_FLAGS "${LEAN_DYN_EXE_LINKER_FLAGS} -rdynamic") + 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() # On Windows, add bcrypt for random number generation if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lbcrypt") set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -lbcrypt") - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lbcrypt") endif() # 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 `leanshared` target - set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} $bindir/libleanshared.dll.a") + # import library created by the `lean` target + set(LEANC_SHARED_LINKER_FLAGS "$bindir/lean.exe.a") elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") - set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -Wl,-undefined,dynamic_lookup") + set(LEANC_SHARED_LINKER_FLAGS "-Wl,-undefined,dynamic_lookup") endif() # Linux ignores undefined symbols in shared libraries by default @@ -378,25 +379,16 @@ 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(${STAGE} GREATER 1) - # reuse C++ parts, which don't change - add_library(leanrt_initial-exec STATIC IMPORTED) - set_target_properties(leanrt_initial-exec PROPERTIES - IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a") - add_library(leanrt STATIC IMPORTED) - set_target_properties(leanrt PROPERTIES - IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a") +if(LEANCPP) 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 "${PREV_STAGE}/runtime/libleanrt_initial-exec.a" "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.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") + COMMAND cmake -E copy_if_different "${LEANCPP}" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a") add_dependencies(leancpp copy-leancpp) else() add_subdirectory(runtime) - + set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(util) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(kernel) @@ -409,77 +401,87 @@ 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 + 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") -# ...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 ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") -else() - set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${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") - 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 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 - 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) - +# 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) + + 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}}") + + 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_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() -configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY) -file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin) +target_link_libraries(leancpp INTERFACE ${EXTRA_LIBS}) -install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin) +configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY) +install(FILES "${CMAKE_BINARY_DIR}/bin/leanc" + DESTINATION bin + PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE) +file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin) +install(FILES ${LEAN_SOURCE_DIR}/bin/leanmake + DESTINATION bin + PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE) +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) @@ -499,12 +501,15 @@ install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include FILES_MATCHING PATTERN "*.h") -if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - install(CODE "execute_process(COMMAND sh -c \"cp $(ldd ${CMAKE_BINARY_DIR}/bin/lean.exe | cut -f3 -d\\\" \\\" | grep mingw) \${CMAKE_INSTALL_PREFIX}/bin\")") -elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") - install(CODE "execute_process(COMMAND sh -c \"cp $(otool -L ${CMAKE_BINARY_DIR}/bin/lean | tail -n +2 | cut -f1 -d\\\" \\\" | grep nix) \${CMAKE_INSTALL_PREFIX}/lib\")") -else() - install(CODE "execute_process(COMMAND sh -c \"cp $(ldd ${CMAKE_BINARY_DIR}/bin/lean | cut -f3 -d\\\" \\\" | grep -Ev 'libc|lean') \${CMAKE_INSTALL_PREFIX}/lib\")") +if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON") + # TODO(Leo): do not hardcode required DLLs. + # For example, we can try to use ldd to retrieve the list of required DLLs. + set(RUNTIME_LIBRARIES + ${MINGW_LOCAL_DIR}/libgmp-10.dll + ${MINGW_LOCAL_DIR}/libwinpthread-1.dll + ${MINGW_LOCAL_DIR}/libgcc_s_seh-1.dll + ${MINGW_LOCAL_DIR}/libstdc++-6.dll) + install(PROGRAMS ${RUNTIME_LIBRARIES} DESTINATION bin) endif() # CPack @@ -522,4 +527,12 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") else() SET(CPACK_GENERATOR ZIP) endif() +# CPack -- Debian +if(STATIC) + SET(CPACK_DEBIAN_PACKAGE_DEPENDS "") +else() + SET(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++-4.8-dev,libgmp-dev") +endif() +SET(CPACK_DEBIAN_PACKAGE_DESCRIPTION "Lean Theorem Prover") +SET(CPACK_DEBIAN_PACKAGE_SECTION "devel") include(CPack) diff --git a/src/bin/leanc.in b/src/bin/leanc.in index 9adaf0caf1..3212193b60 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -17,14 +17,12 @@ set -e bindir=$(dirname $0) cflags=("-I$bindir/../include" @LEANC_EXTRA_FLAGS@) -ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) +ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}") ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@) args=("$@") for arg in "$@"; do # passed -shared ~> switch to shared linker flags [[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) && args=("-x" "c" "$@" "-x" "none") - # linking against libleanshared explicitly (or linking libleanshared itself) ~> do not link against static stdlib - [[ $arg == "-lleanshared" || $arg == *libleanshared.* ]] && ldflags_ext=() # Note the `-x c` for treating all input as C code [[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() && args=("-x" "c" "$@" "-x" "none") [[ $arg == "--print-cflags" ]] && echo "${cflags[@]}" && exit diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp index 753c66065c..72d278e695 100644 --- a/src/initialize/init.cpp +++ b/src/initialize/init.cpp @@ -18,7 +18,6 @@ Author: Leonardo de Moura namespace lean { extern "C" object* initialize_Init(object* w); -extern "C" object* initialize_Std(object* w); extern "C" object* initialize_Lean(object* w); /* Initializes the Lean runtime. Before executing any code which uses the Lean package, @@ -28,7 +27,6 @@ extern "C" void lean_initialize() { save_stack_info(); initialize_util_module(); consume_io_result(initialize_Init(io_mk_world())); - consume_io_result(initialize_Std(io_mk_world())); consume_io_result(initialize_Lean(io_mk_world())); initialize_kernel_module(); init_default_print_fn(); diff --git a/src/lean.mk.in b/src/lean.mk.in index 92fd1f97a3..8f6e9e218a 100644 --- a/src/lean.mk.in +++ b/src/lean.mk.in @@ -16,7 +16,6 @@ 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) @@ -30,7 +29,7 @@ DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend)) export LEAN_PATH += @LEAN_PATH_SEPARATOR@$(OLEAN_OUT) OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean)) -SHELL = /usr/bin/env bash -euo pipefail +SHELL = /usr/bin/env bash -eo pipefail .PHONY: all bin lib depends clean @@ -62,12 +61,10 @@ 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: $(C_OUT)/%.c +$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.c ifdef CMAKE_LIKE_OUTPUT @echo "[ ] Building $<" endif @@ -97,6 +94,4 @@ clean: .PRECIOUS: $(TEMP_OUT)/%.c -ifndef C_ONLY include $(DEPS) -endif diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 91dd9e7e4a..f61fe4ca00 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -31,7 +31,6 @@ functions, which have a (relatively) homogeneous ABI that we can use without run #ifdef LEAN_WINDOWS #include #undef ERROR // thanks, wingdi.h -#include #else #include #endif @@ -287,16 +286,7 @@ void print_value(std::ostream & ios, value const & v, type t) { void * lookup_symbol_in_cur_exe(char const * sym) { #ifdef LEAN_WINDOWS - HMODULE hmods[128]; // 128 modules should be enough for everyone - DWORD bytes_needed; - lean_always_assert(EnumProcessModules(GetCurrentProcess(), hmods, sizeof(hmods), &bytes_needed)); - for (int i = 0; i < bytes_needed / sizeof(HMODULE); i++) { - void * addr = reinterpret_cast(GetProcAddress(hmods[i], sym)); - if (addr) { - return addr; - } - } - return nullptr; + return reinterpret_cast(GetProcAddress(GetModuleHandle(nullptr), sym)); #else return dlsym(RTLD_DEFAULT, sym); #endif diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 6f2293c13a..8735d13235 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -3,29 +3,15 @@ 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(leanrt_initial-exec STATIC ${RUNTIME_OBJS}) -set_target_properties(leanrt_initial-exec PROPERTIES - ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}) - -# The above library, like all other C++ code, is built using `-ftls-model=initial-exec`, which is necessary for linking it into `leanshared`, -# 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} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -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 DEPENDS ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libleanrt.a) - +add_library(runtime OBJECT ${RUNTIME_OBJS}) +add_library(leanruntime ${RUNTIME_OBJS}) if(LLVM) + string(REPLACE ";" " " RUNTIME_OBJS_STR "${RUNTIME_OBJS};lean_inlines.c") add_custom_command( - OUTPUT libleanrt.bc + OUTPUT libleanruntime.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}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${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 libleanruntime.bc" VERBATIM) - add_custom_target(runtime_bc DEPENDS libleanrt.bc) + add_custom_target(runtime_bc DEPENDS libleanruntime.bc) endif() diff --git a/src/shared/init.cpp b/src/shared/init.cpp new file mode 100644 index 0000000000..98c325b8a7 --- /dev/null +++ b/src/shared/init.cpp @@ -0,0 +1,11 @@ +/* +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 63026b639f..eb14a4a882 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -12,24 +12,38 @@ if(LLVM) set(LLVM_SYSTEM_LIBS "-lz") endif() if(${STATIC} AND NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")) - set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} `llvm-config --link-static --ldflags --libs nativecodegen` -Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic") + set(LEAN_EXE_LINKER_FLAGS "`llvm-config --link-static --ldflags --libs nativecodegen` -Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic") else() - set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} `llvm-config --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}") + set(LEAN_EXE_LINKER_FLAGS "`llvm-config --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}") endif() if (${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} -lole32 -luuid") endif() +else() + set(LEAN_EXE_LINKER_FLAGS "") 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 "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}" + 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}" VERBATIM - DEPENDS leanshared shell $,runtime_bc,>) + DEPENDS Init Std Lean leancpp shell $,runtime_bc,>) add_custom_target(lean ALL DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}) +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") @@ -104,13 +118,18 @@ FOREACH(T_OUT ${LEANBENCHTESTS}) COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") ENDFOREACH(T_OUT) -file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean") -FOREACH(T ${LEANINTERPTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanplugintest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") -ENDFOREACH(T) +# LEAN PLUGIN TESTS +if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Windows") + # We temporarily disabled these tests on Windows because of problems in the shared library generation. + # The problem happened when the clang version has changed from mingw-w64-x86_64-clang-11.0.0-6 to mingw-w64-x86_64-clang-11.0.0-7 in the CI + file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean") + FOREACH(T ${LEANINTERPTESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanplugintest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" + COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + ENDFOREACH(T) +endif() # LEAN TESTS using --trust=0 file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean") @@ -199,4 +218,4 @@ add_test(NAME leanpkgtest_user_attr_app set -eu export PATH=${LEAN_BIN}:$PATH find . -name '*.olean' -delete - leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr") + leanmake bin LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS}' && build/bin/UserAttr") diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 8ff577b5ad..acc59d2615 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -3,6 +3,9 @@ SHELL := /usr/bin/env bash -euo pipefail # any absolute path to the stdlib breaks the Makefile export LEAN_PATH= +# link GMP statically if STATIC=ON +export LEANC_GMP=${GMP_LIBRARIES} + # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage # MORE_DEPS: rebuild the stdlib whenever the compiler has changed LEANMAKE_OPTS=\ @@ -16,24 +19,11 @@ 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\ - $(MORE_LEANMAKE_OPTS) + CMAKE_LIKE_OUTPUT=1 -.PHONY: Init Std Lean leanshared Leanpkg - -Init: +stdlib: # 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) - -leanshared: Init Std Lean - @mkdir -p "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" || true - "${LEAN_BIN}/leanc" -x none -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} - -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}' + +"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS="${CMAKE_EXE_LINKER_FLAGS}" diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 8f86f412e3..679fb3800d 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -38,13 +38,13 @@ max_runs: 1 runner: output - attributes: - description: libleanshared.so + description: bin/lean tags: [deterministic, fast] run_config: cmd: | set -eu echo -n 'binary size: ' - wc -c ${BUILD:-../../build/release}/stage2/lib/lean/libleanshared.so | cut -d' ' -f 1 + wc -c ${BUILD:-../../build/release}/stage2/bin/lean | cut -d' ' -f 1 max_runs: 1 runner: output - attributes: