Revert "feat: reintroduce libleanshared, link lean & leanpkg against it"
This commit is contained in:
Sebastian Ullrich
parent
49520aa2ee
commit
ccbc9d00db
18 changed files with 217 additions and 230 deletions
28
.github/workflows/ci.yml
vendored
28
.github/workflows/ci.yml
vendored
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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" ];
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
})
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2,10 +2,19 @@
|
|||
set -euo pipefail
|
||||
|
||||
rm -r stage0 || true
|
||||
mkdir -p stage0/stdlib/
|
||||
cat <<EOF >> 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 <<EOF >> 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/{}'
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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} $<TARGET_OBJECTS:runtime>)
|
||||
add_subdirectory(util)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:util>)
|
||||
add_subdirectory(kernel)
|
||||
|
|
@ -409,77 +401,87 @@ else()
|
|||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
|
||||
add_subdirectory(initialize)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
|
||||
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 $<IF:$<EQUAL:${STAGE},0>,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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
|
|||
#ifdef LEAN_WINDOWS
|
||||
#include <windows.h>
|
||||
#undef ERROR // thanks, wingdi.h
|
||||
#include <psapi.h>
|
||||
#else
|
||||
#include <dlfcn.h>
|
||||
#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<void *>(GetProcAddress(hmods[i], sym));
|
||||
if (addr) {
|
||||
return addr;
|
||||
}
|
||||
}
|
||||
return nullptr;
|
||||
return reinterpret_cast<void *>(GetProcAddress(GetModuleHandle(nullptr), sym));
|
||||
#else
|
||||
return dlsym(RTLD_DEFAULT, sym);
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -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$<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 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$<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}; 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"
|
||||
VERBATIM)
|
||||
add_custom_target(runtime_bc DEPENDS libleanrt.bc)
|
||||
add_custom_target(runtime_bc DEPENDS libleanruntime.bc)
|
||||
endif()
|
||||
|
|
|
|||
11
src/shared/init.cpp
Normal file
11
src/shared/init.cpp
Normal file
|
|
@ -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;
|
||||
}
|
||||
|
|
@ -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 $<TARGET_OBJECTS:shell> -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 $<TARGET_OBJECTS:shell> ${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 $<IF:$<BOOL:${LLVM}>,runtime_bc,>)
|
||||
DEPENDS Init Std Lean leancpp shell $<IF:$<BOOL:${LLVM}>,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")
|
||||
|
|
|
|||
|
|
@ -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}"
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue