From 37ff2414673bb599d6db98b42d340fa3c9130ee9 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Thu, 25 Jul 2019 14:41:40 -0700 Subject: [PATCH] feat(CMakeLists): Add option to link in LLVM. This updates cmake and Lean to link against the LLVM libraries. --- azure-pipelines.yml | 2 +- bin/leanc.in | 3 ++- derivation.nix | 8 ++++---- script/ci.sh | 2 +- src/CMakeLists.txt | 27 +++++++++++++++++++++++++++ src/shell/lean.cpp | 8 ++++++++ 6 files changed, 43 insertions(+), 7 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index e1b941f71c..5396b81030 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -39,7 +39,7 @@ jobs: steps: - script: | choco install -y msys2 - C:\tools\msys64\usr\bin\bash -lc "pacman --noconfirm -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc git diffutils" + C:\tools\msys64\usr\bin\bash -lc "pacman --noconfirm -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-gcc mingw-w64-x86_64-clang mingw-w64-x86_64-polly git diffutils" displayName: Setup - script: | C:\tools\msys64\usr\bin\bash -l ./script/ci.sh diff --git a/bin/leanc.in b/bin/leanc.in index 6650661a25..283b42d126 100644 --- a/bin/leanc.in +++ b/bin/leanc.in @@ -17,4 +17,5 @@ for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do done [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!" # NOTE: leanstatic and leanstdlib are cyclically dependent -$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument + +$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument diff --git a/derivation.nix b/derivation.nix index c8583b36da..0955392d7b 100644 --- a/derivation.nix +++ b/derivation.nix @@ -1,6 +1,6 @@ -{ stdenv, cmake, python, gmp }: +{ clangStdenv, cmake, llvm, python, gmp }: -stdenv.mkDerivation rec { +clangStdenv.mkDerivation rec { name = "lean-${version}"; version = "local"; @@ -8,7 +8,7 @@ stdenv.mkDerivation rec { src = builtins.fetchGit { url = ./.; }; nativeBuildInputs = [ cmake python ]; - buildInputs = [ gmp ]; + buildInputs = [ gmp llvm ]; enableParallelBuilding = true; preConfigure = '' @@ -18,7 +18,7 @@ stdenv.mkDerivation rec { patchShebangs ../../bin ''; - meta = with stdenv.lib; { + meta = with clangStdenv.lib; { description = "Automatic and interactive theorem prover"; homepage = https://leanprover.github.io/; license = licenses.asl20; diff --git a/script/ci.sh b/script/ci.sh index eb6ef0c61f..408eb8f2a1 100755 --- a/script/ci.sh +++ b/script/ci.sh @@ -2,7 +2,7 @@ set -e mkdir build cd build -eval cmake ../src $CMAKE_OPTIONS +eval cmake ../src -DLLVM=ON $CMAKE_OPTIONS cmake --build . # -T to create .xml file ctest -j8 --output-on-failure --no-compress-output -T Test diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b5e87914ec..2f0fd9994a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -32,6 +32,8 @@ option(TCMALLOC "TCMALLOC" OFF) option(JEMALLOC "JEMALLOC" OFF) # When OFF we disable JSON support to support older compilers option(JSON "JSON" ON) +# When OFF we disable LLVM support +option(JSON "LLVM" ON) # When cross-compiling, we do not compile the standard library since # the executable will not work on the host machine @@ -172,6 +174,9 @@ if((${CYGWIN} EQUAL "1") OR (${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}") +else() + # Windows does not support pthread or fPIC + set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -pthread -fPIC") endif() if("${CYGWIN}" EQUAL "1") @@ -205,6 +210,23 @@ if(AUTO_THREAD_FINALIZATION AND NOT MSVC) set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION") endif() +if(LLVM) + find_package(LLVM REQUIRED CONFIG) + message(STATUS "Found CLANG ${CLANG_PACKAGE_VERSION}") + message(STATUS "Using ClangConfig.cmake in: ${CLANG_DIR}") + message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") + message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}") + + include_directories(${LLVM_INCLUDE_DIRS}) + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_LLVM") + + # Find the libraries that correspond to the LLVM components + # that we wish to use and define llvm_libs + llvm_map_components_to_libnames(llvm_libs nativecodegen) +else() + message(WARNING "Disabling LLVM support. JIT compilation will not be available") +endif() + if(STATIC) message(STATUS "Creating a static executable") if (MULTI_THREAD AND ${CMAKE_SYSTEM_NAME} MATCHES "Linux") @@ -463,6 +485,11 @@ add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS}) add_library(leanstdlib STATIC IMPORTED) target_link_libraries(leanstatic leanstdlib ${EXTRA_LIBS}) +if(LLVM) + target_link_libraries(leanstatic_stage0 ${llvm_libs}) + target_link_libraries(leanstatic ${llvm_libs}) +endif() + ADD_CUSTOM_TARGET(bin_lib ALL COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin" COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "$" "$" "${LEAN_SOURCE_DIR}/../bin" diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 4de59fb8f1..982574abba 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -55,6 +55,10 @@ Author: Leonardo de Moura #endif #include "githash.h" // NOLINT +#if defined(LEAN_LLVM) +#include +#endif + #ifdef _MSC_VER // extremely simple implementation of getopt.h enum arg_opt { no_argument, required_argument, optional_argument }; @@ -353,6 +357,10 @@ int main(int argc, char ** argv) { #if defined(LEAN_JSON) bool json_output = false; #endif +#if defined(LEAN_LLVM) + // Initialize LLVM backends for native code generation. + llvm::InitializeNativeTarget(); +#endif init_search_path();