feat(CMakeLists): Add option to link in LLVM.

This updates cmake and Lean to link against the LLVM libraries.

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

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

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;

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

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} "$<TARGET_FILE:leanstdlib>" "$<TARGET_FILE:leanstatic>" "${LEAN_SOURCE_DIR}/../bin"

src/shell/lean.cpp

@@ -55,6 +55,10 @@ Author: Leonardo de Moura
 #endif
 #include "githash.h" // NOLINT
 
+#if defined(LEAN_LLVM)
+#include <llvm/Support/TargetSelect.h>
+#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();