From: Mathias Preiner Date: Fri, 6 Dec 2019 14:48:04 +0000 (-0800) Subject: contrib: Setup all dependencies in deps/ directory. (#3534) X-Git-Tag: cvc5-1.0.0~3792 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=008d6b51baec353f45324e1d9407d898866cf688;p=cvc5.git contrib: Setup all dependencies in deps/ directory. (#3534) --- diff --git a/CMakeLists.txt b/CMakeLists.txt index c2ce3e6ac..7d8b6d9ab 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -32,6 +32,51 @@ set(CMAKE_CXX_EXTENSIONS OFF) # plugins. set(CMAKE_EXPORT_COMPILE_COMMANDS ON) +#-----------------------------------------------------------------------------# +# Policies + +# Required for FindGLPK since it sets CMAKE_REQUIRED_LIBRARIES +if(POLICY CMP0075) + cmake_policy(SET CMP0075 NEW) +endif() + +#-----------------------------------------------------------------------------# +# Tell CMake where to find our dependencies + +if(ABC_DIR) + list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}") +endif() +if(ANTLR_DIR) + list(APPEND CMAKE_PREFIX_PATH "${ANTLR_DIR}") +endif() +if(CADICAL_DIR) + list(APPEND CMAKE_PREFIX_PATH "${CADICAL_DIR}") +endif() +if(CRYPTOMINISAT_DIR) + list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}") +endif() +if(CXXTEST_DIR) + list(APPEND CMAKE_PREFIX_PATH "${CXXTEST_DIR}") +endif() +if(DRAT2ER_DIR) + list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}") +endif() +if(GLPK_DIR) + list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}") +endif() +if(GMP_DIR) + list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}") +endif() +if(LFSC_DIR) + list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}") +endif() +if(SYMFPU_DIR) + list(APPEND CMAKE_PREFIX_PATH "${SYMFPU_DIR}") +endif() + +# By default the contrib/get-* scripts install dependencies to deps/install. +list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install") + #-----------------------------------------------------------------------------# set(INCLUDE_INSTALL_DIR include) @@ -286,7 +331,6 @@ else() find_package(PythonInterp REQUIRED) endif() -set(GMP_HOME ${GMP_DIR}) find_package(GMP REQUIRED) if(ENABLE_ASAN) @@ -383,13 +427,11 @@ if(ENABLE_VALGRIND) endif() if(USE_ABC) - set(ABC_HOME "${ABC_DIR}") find_package(ABC REQUIRED) add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS}) endif() if(USE_CADICAL) - set(CaDiCaL_HOME ${CADICAL_DIR}) find_package(CaDiCaL REQUIRED) add_definitions(-DCVC4_USE_CADICAL) endif() @@ -411,27 +453,23 @@ if(USE_CRYPTOMINISAT) if(THREADS_HAVE_PTHREAD_ARG) add_c_cxx_flag(-pthread) endif() - set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR}) find_package(CryptoMiniSat REQUIRED) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() if(USE_DRAT2ER) - set(Drat2Er_HOME ${DRAT2ER_DIR}) find_package(Drat2Er REQUIRED) add_definitions(-DCVC4_USE_DRAT2ER) endif() if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") - set(GLPK_HOME ${GLPK_DIR}) find_package(GLPK REQUIRED) add_definitions(-DCVC4_USE_GLPK) endif() if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) - set(LFSC_HOME ${LFSC_DIR}) find_package(LFSC REQUIRED) add_definitions(-DCVC4_USE_LFSC) endif() @@ -446,7 +484,6 @@ if(USE_READLINE) endif() if(USE_SYMFPU) - set(SymFPU_HOME ${SYMFPU_DIR}) find_package(SymFPU REQUIRED) add_definitions(-DCVC4_USE_SYMFPU) set(CVC4_USE_SYMFPU 1) diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake index c44019739..a6f182654 100644 --- a/cmake/FindABC.cmake +++ b/cmake/FindABC.cmake @@ -4,26 +4,12 @@ # ABC_LIBRARIES - Libraries needed to use ABC # ABC_ARCH_FLAGS - Platform specific compile flags - -# Check default location of ABC built with contrib/get-abc. -if(NOT ABC_HOME) - set(ABC_HOME ${PROJECT_SOURCE_DIR}/abc/alanmi-abc-53f39c11b58d) -endif() - -# Note: We don't check the system version since ABC does not provide a default -# install rule. -find_path(ABC_INCLUDE_DIR - NAMES base/abc/abc.h - PATHS ${ABC_HOME}/src - NO_DEFAULT_PATH) -find_library(ABC_LIBRARIES - NAMES abc - PATHS ${ABC_HOME} - NO_DEFAULT_PATH) -find_program(ABC_ARCH_FLAGS_PROG - NAMES arch_flags - PATHS ${ABC_HOME} - NO_DEFAULT_PATH) +# Note: contrib/get-abc copies header files to deps/install/include/abc. +# However, includes in ABC headers are not prefixed with "abc/" and therefore +# we have to look for headers in include/abc instead of include/. +find_path(ABC_INCLUDE_DIR NAMES base/abc/abc.h PATH_SUFFIXES abc) +find_library(ABC_LIBRARIES NAMES abc) +find_program(ABC_ARCH_FLAGS_PROG NAMES arch_flags) if(ABC_ARCH_FLAGS_PROG) execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG} diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake index 5f574247b..e12af826a 100644 --- a/cmake/FindANTLR.cmake +++ b/cmake/FindANTLR.cmake @@ -4,33 +4,9 @@ # ANTLR_INCLUDE_DIR - the ANTLR include directory # ANTLR_LIBRARIES - Libraries needed to use ANTLR - -# Check default location of ANTLR built with contrib/get-antlr-3.4. -# If the user provides a directory we will not search the default paths and -# fail if ANTLR was not found in the specified directory. -if(NOT ANTLR_HOME) - set(ANTLR_HOME ${PROJECT_SOURCE_DIR}/antlr-3.4) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_program(ANTLR_BINARY - NAMES antlr3 - PATHS ${ANTLR_HOME}/bin - NO_DEFAULT_PATH) -find_path(ANTLR_INCLUDE_DIR - NAMES antlr3.h - PATHS ${ANTLR_HOME}/include - NO_DEFAULT_PATH) -find_library(ANTLR_LIBRARIES - NAMES antlr3c antlr3c-static - PATHS ${ANTLR_HOME}/lib - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_program(ANTLR_BINARY NAMES antlr3) - find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h) - find_library(ANTLR_LIBRARIES NAMES antlr3c) -endif() +find_program(ANTLR_BINARY NAMES antlr3) +find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h) +find_library(ANTLR_LIBRARIES NAMES antlr3c antlr3c-static) # Check if antlr3FileStreamNew is available. If not we have to # define CVC4_ANTLR3_OLD_INPUT_STREAM (src/parser/CMakeLists.txt). diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index bd7de319a..5ca7ce7b0 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -3,28 +3,8 @@ # CaDiCaL_INCLUDE_DIR - the CaDiCaL include directory # CaDiCaL_LIBRARIES - Libraries needed to use CaDiCaL - -# Check default location of CaDiCaL built with contrib/get-cadical. -# If the user provides a directory we will not search the default paths and -# fail if CaDiCaL was not found in the specified directory. -if(NOT CaDiCaL_HOME) - set(CaDiCaL_HOME ${PROJECT_SOURCE_DIR}/cadical) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_path(CaDiCaL_INCLUDE_DIR - NAMES cadical.hpp - PATHS ${CaDiCaL_HOME}/src - NO_DEFAULT_PATH) -find_library(CaDiCaL_LIBRARIES - NAMES cadical - PATHS ${CaDiCaL_HOME}/build - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp) - find_library(CaDiCaL_LIBRARIES NAMES cadical) -endif() +find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp) +find_library(CaDiCaL_LIBRARIES NAMES cadical) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(CaDiCaL diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index d96c54eb3..44b30ba7e 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -4,27 +4,8 @@ # CryptoMiniSat_LIBRARIES - Libraries needed to use CryptoMiniSat -# Check default location of CryptoMiniSat built with contrib/get-cryptominisat. -# If the user provides a directory we will not search the default paths and -# fail if CryptoMiniSat was not found in the specified directory. -if(NOT CryptoMiniSat_HOME) - set(CryptoMiniSat_HOME ${PROJECT_SOURCE_DIR}/cryptominisat5/build) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_path(CryptoMiniSat_INCLUDE_DIR - NAMES cryptominisat5/cryptominisat.h - PATHS ${CryptoMiniSat_HOME}/include ${CryptoMiniSat_HOME}/cmsat5-src - NO_DEFAULT_PATH) -find_library(CryptoMiniSat_LIBRARIES - NAMES cryptominisat5 - PATHS ${CryptoMiniSat_HOME}/lib - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h) - find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5) -endif() +find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h) +find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(CryptoMiniSat diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake index a7c2538a5..dc6f2a9b0 100644 --- a/cmake/FindDrat2Er.cmake +++ b/cmake/FindDrat2Er.cmake @@ -3,26 +3,9 @@ # Drat2Er_INCLUDE_DIR - the Drat2Er include directory # Drat2Er_LIBRARIES - Libraries needed to use Drat2Er - -# Check default location of Drat2Er built with contrib/get-drat2er. -# If the user provides a directory we will not search the default paths and -# fail if Drat2Er was not found in the specified directory. -if(NOT Drat2Er_HOME) - set(Drat2Er_HOME ${PROJECT_SOURCE_DIR}/drat2er/build/install) -endif() - -find_path(Drat2Er_INCLUDE_DIR - NAMES drat2er.h - PATHS ${Drat2Er_HOME}/include - NO_DEFAULT_PATH) -find_library(Drat2Er_LIBRARIES - NAMES libdrat2er.a - PATHS ${Drat2Er_HOME}/lib - NO_DEFAULT_PATH) -find_library(DratTrim_LIBRARIES - NAMES libdrat-trim.a - PATHS ${Drat2Er_HOME}/lib - NO_DEFAULT_PATH) +find_path(Drat2Er_INCLUDE_DIR NAMES drat2er.h) +find_library(Drat2Er_LIBRARIES NAMES libdrat2er.a) +find_library(DratTrim_LIBRARIES NAMES libdrat-trim.a) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(Drat2Er diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake index 1587ca821..390992639 100644 --- a/cmake/FindGLPK.cmake +++ b/cmake/FindGLPK.cmake @@ -4,27 +4,8 @@ # GLPK_LIBRARIES - Libraries needed to use GLPK -# Check default location of GLPK built with contrib/get-glpk-cut-log. -# If the user provides a directory we will not search the default paths and -# fail if GLPK was not found in the specified directory. -if(NOT GLPK_HOME) - set(GLPK_HOME ${PROJECT_SOURCE_DIR}/glpk-cut-log) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_path(GLPK_INCLUDE_DIR - NAMES glpk.h - PATHS ${GLPK_HOME}/include - NO_DEFAULT_PATH) -find_library(GLPK_LIBRARIES - NAMES glpk - PATHS ${GLPK_HOME}/lib - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_path(GLPK_INCLUDE_DIR NAMES glpk.h) - find_library(GLPK_LIBRARIES NAMES glpk) -endif() +find_path(GLPK_INCLUDE_DIR NAMES glpk.h) +find_library(GLPK_LIBRARIES NAMES glpk) # Check if we really have GLPK-cut-log. if(GLPK_INCLUDE_DIR) diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 8125a583b..08cee9690 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -3,28 +3,8 @@ # GMP_INCLUDE_DIR - the GMP include directory # GMP_LIBRARIES - Libraries needed to use GMP - -# Check default location of GMP built with contrib/get-gmp. -# If the user provides a directory we will not search the default paths and -# fail if GMP was not found in the specified directory. -if(NOT GMP_HOME) - set(GMP_HOME ${PROJECT_SOURCE_DIR}/gmp-6.1.2) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_path(GMP_INCLUDE_DIR - NAMES gmp.h gmpxx.h - PATHS ${GMP_HOME}/include - NO_DEFAULT_PATH) -find_library(GMP_LIBRARIES - NAMES gmp - PATHS ${GMP_HOME}/lib - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h) - find_library(GMP_LIBRARIES NAMES gmp) -endif() +find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h) +find_library(GMP_LIBRARIES NAMES gmp) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index 7a666839b..6135c7891 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -3,28 +3,8 @@ # LFSC_INCLUDE_DIR - the LFSC include directory # LFSC_LIBRARIES - Libraries needed to use LFSC - -# Check default location of LFSC built with contrib/get-lfsc. -# If the user provides a directory we will not search the default paths and -# fail if LFSC was not found in the specified directory. -if(NOT LFSC_HOME) - set(LFSC_HOME ${PROJECT_SOURCE_DIR}/lfsc-checker/install) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_path(LFSC_INCLUDE_DIR - NAMES lfscc.h - PATHS ${LFSC_HOME}/include - NO_DEFAULT_PATH) -find_library(LFSC_LIBRARIES - NAMES lfscc - PATHS ${LFSC_HOME}/lib - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_path(LFSC_INCLUDE_DIR NAMES lfscc.h) - find_library(LFSC_LIBRARIES NAMES lfscc) -endif() +find_path(LFSC_INCLUDE_DIR NAMES lfscc.h) +find_library(LFSC_LIBRARIES NAMES lfscc) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(LFSC diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index f0f9ebf0f..dd9dbe113 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -2,23 +2,7 @@ # SymFPU_FOUND - system has SymFPU lib # SymFPU_INCLUDE_DIR - the SymFPU include directory - -# Check default location of SymFPU built with contrib/get-symfpu. -# If the user provides a directory we will not search the default paths and -# fail if SymFPU was not found in the specified directory. -if(NOT SymFPU_HOME) - set(SymFPU_HOME ${PROJECT_SOURCE_DIR}/symfpu-CVC4) - set(CHECK_SYSTEM_VERSION TRUE) -endif() - -find_path(SymFPU_INCLUDE_DIR - NAMES symfpu/core/unpackedFloat.h - PATHS ${SymFPU_HOME} - NO_DEFAULT_PATH) - -if(CHECK_SYSTEM_VERSION) - find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h) -endif() +find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(SymFPU DEFAULT_MSG SymFPU_INCLUDE_DIR) diff --git a/contrib/get-abc b/contrib/get-abc index 5d3f32fb5..d69af9ef8 100755 --- a/contrib/get-abc +++ b/contrib/get-abc @@ -2,19 +2,12 @@ # source "$(dirname "$0")/get-script-header.sh" -if [ -e abc ]; then - echo 'error: file or directory "abc" exists; please move it out of the way.' >&2 - exit 1 -fi - +ABC_DIR="$DEPS_DIR/abc" commit=53f39c11b58d -mkdir abc -cd abc -webget https://bitbucket.org/alanmi/abc/get/$commit.tar.gz abc-$commit.tar.gz -gunzip -f abc-$commit.tar.gz -tar xfv abc-$commit.tar -cd alanmi-abc-$commit +check_dep_dir "$ABC_DIR" +setup_dep "https://bitbucket.org/alanmi/abc/get/$commit.tar.gz" "$ABC_DIR" +cd "$ABC_DIR" # Strip out libSupport.c, it is in charge of loading extensions and we # don't want different behavior based on ABC_LIB_PATH, or based on what @@ -28,8 +21,17 @@ sed 's,\( *\)\(.*Libs_Init(\),\1//\2,;s,\( *\)\(.*Libs_End(\),\1//\2,' src/base/ # These aren't necessary for our usage and we don't want the dependencies. make -j$(nproc) libabc.a OPTFLAGS=-O ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1 mv libabc.a libabc-static.a +install_lib libabc-static.a make clean + make -j$(nproc) libabc.a OPTFLAGS='-O -fPIC' ABC_USE_NO_READLINE=1 ABC_USE_NO_PTHREADS=1 +install_lib libabc.a +install_bin arch_flags + +# Copy headers and preserve subdirectories +cd src +mkdir -p "$INSTALL_INCLUDE_DIR/abc" +cp --parents $(find . -name '*.h') "$INSTALL_INCLUDE_DIR/abc" echo echo ===================== Now configure CVC4 with ===================== diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index ecc92d998..9ab0695b7 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -1,20 +1,20 @@ #!/usr/bin/env bash # source "$(dirname "$0")/get-script-header.sh" -ANTLR_HOME_DIR=antlr-3.4 +ANTLR_HOME_DIR="$DEPS_DIR/antlr-3.4" if [ -z "${BUILD_TYPE}" ]; then BUILD_TYPE="--disable-shared --enable-static" fi if [ -z "${MACHINE_TYPE}" ]; then - CONFIG_GUESS_SCRIPT=$ANTLR_HOME_DIR/config.guess - if ! [ -e ${CONFIG_GUESS_SCRIPT} ]; then - mkdir -p $ANTLR_HOME_DIR + CONFIG_GUESS_SCRIPT="$ANTLR_HOME_DIR/config.guess" + if ! [ -e "${CONFIG_GUESS_SCRIPT}" ]; then + mkdir -p "$ANTLR_HOME_DIR" # Attempt to download once webget 'http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.guess;hb=HEAD' $CONFIG_GUESS_SCRIPT - if [ -e $CONFIG_GUESS_SCRIPT ]; then - chmod +x $CONFIG_GUESS_SCRIPT + if [ -e "$CONFIG_GUESS_SCRIPT" ]; then + chmod +x "$CONFIG_GUESS_SCRIPT" else echo "$(basename $0): I need the file config/config.guess to tell MACHINE_TYPE" >&2 echo "Try running ./autogen.sh, or set the MACHINE_TYPE environment variable" >&2 @@ -26,36 +26,33 @@ if [ -z "${MACHINE_TYPE}" ]; then MACHINE_TYPE=$(${CONFIG_GUESS_SCRIPT} | sed 's,-.*,,') fi -set -x -mkdir -p $ANTLR_HOME_DIR/share/java -mkdir -p $ANTLR_HOME_DIR/bin -mkdir -p $ANTLR_HOME_DIR/src -cd $ANTLR_HOME_DIR || exit 1 -webget https://www.antlr3.org/download/antlr-3.4-complete.jar share/java/antlr-3.4-complete.jar -webget https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz src/libantlr3c-3.4.tar.gz -tee bin/antlr3 < Makefile make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" make install -cd ../.. -mv lib/libantlr3c.la lib/libantlr3c.la.orig -awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}' < lib/libantlr3c.la.orig > lib/libantlr3c.la -set +x -cd .. +mv "$INSTALL_LIB_DIR/libantlr3c.la" "$INSTALL_LIB_DIR/libantlr3c.la.orig" -# echo -# echo Invalidating generated parsers.. -# touch src/parser/*/*.g +awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}' < "$INSTALL_LIB_DIR/libantlr3c.la.orig" > "$INSTALL_LIB_DIR/libantlr3c.la" +rm "$INSTALL_LIB_DIR/libantlr3c.la.orig" -if [ ${MACHINE_TYPE} == 'x86_64' ]; then +if [ "${MACHINE_TYPE}" == 'x86_64' ]; then # 64-bit stuff here echo ============== WARNING ==================== echo The script guessed that this machine is 64 bit. @@ -105,7 +94,7 @@ if [ ${MACHINE_TYPE} == 'x86_64' ]; then else # 32-bit stuff here - echo ============== WARNING ==================== + echo ============== WARNING ==================== echo The script guessed that this machine is 32 bit. echo If antlr should be built as 64 bit \(i.e. -m64\), echo please rerun the script as diff --git a/contrib/get-cadical b/contrib/get-cadical index 6cc1208c6..8c512ad28 100755 --- a/contrib/get-cadical +++ b/contrib/get-cadical @@ -2,23 +2,21 @@ # source "$(dirname "$0")/get-script-header.sh" -if [ -e cadical ]; then - echo 'error: file or directory "cadical" exists; please move it out of the way.' >&2 - exit 1 -fi - +CADICAL_DIR="$DEPS_DIR/cadical" version="rel-1.0.3" -webget "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "cadical-$version.tar.gz" -tar xfvz "cadical-$version.tar.gz" -rm "cadical-$version.tar.gz" -mv "cadical-$version" cadical -cd cadical +check_dep_dir "$CADICAL_DIR" +setup_dep \ + "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "$CADICAL_DIR" +cd "$CADICAL_DIR" CXXFLAGS="-fPIC" ./configure && make -j$(nproc) +install_lib build/libcadical.a +install_includes src/cadical.hpp + echo -echo "Using CaDiCaL commit $commit" +echo "Using CaDiCaL version $version" echo echo ===================== Now configure CVC4 with ===================== echo ./configure.sh --cadical diff --git a/contrib/get-cryptominisat b/contrib/get-cryptominisat index 379d75df1..2b85e1a91 100755 --- a/contrib/get-cryptominisat +++ b/contrib/get-cryptominisat @@ -2,28 +2,25 @@ # source "$(dirname "$0")/get-script-header.sh" -if [ -e cryptominisat5 ]; then - echo 'error: file or directory "cryptominisat5" exists; please move it out of the way.' >&2 - exit 1 -fi - +CMS_DIR="$DEPS_DIR/cryptominisat5" version="5.6.3" -webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz -tar xfvz cryptominisat-$version.tar.gz -rm cryptominisat-$version.tar.gz -mv cryptominisat-$version cryptominisat5 +check_dep_dir "$CMS_DIR" +setup_dep \ + "https://github.com/msoos/cryptominisat/archive/$version.tar.gz" \ + "$CMS_DIR" +cd "$CMS_DIR" -cd cryptominisat5 mkdir build cd build - cmake -DENABLE_PYTHON_INTERFACE=OFF \ -DSTATICCOMPILE=ON \ -DNOM4RI=ON \ + -DONLY_SIMPLE=ON \ + -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" \ .. -make libcryptominisat5 -j$(nproc) +make install -j$(nproc) echo echo ===================== Now configure CVC4 with ===================== diff --git a/contrib/get-drat2er b/contrib/get-drat2er index 52c663ab3..f04365890 100755 --- a/contrib/get-drat2er +++ b/contrib/get-drat2er @@ -1,24 +1,20 @@ #!/usr/bin/env bash # source "$(dirname "$0")/get-script-header.sh" -if [ -e drat2er ]; then - echo 'error: file or directory "drat2er" exists; please move it out of the way.' >&2 - exit 1 -fi -git clone https://github.com/alex-ozdemir/drat2er.git +DRAT2ER_DIR="$DEPS_DIR/drat2er" +commit=521caf16149df3dfa46f700ec1fab56f8cc12a18 -cd drat2er - -git checkout api +check_dep_dir "$DRAT2ER_DIR" +setup_dep \ + "https://github.com/alex-ozdemir/drat2er/archive/$commit.tar.gz" \ + "$DRAT2ER_DIR" +cd "$DRAT2ER_DIR" mkdir build - cd build - -cmake .. -DCMAKE_INSTALL_PREFIX=$(pwd)/install - -make install +cmake .. -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" +make install -j$(nproc) echo echo ===================== Now configure CVC4 with ===================== diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log index 85ea643a9..16acf97ae 100755 --- a/contrib/get-glpk-cut-log +++ b/contrib/get-glpk-cut-log @@ -2,32 +2,28 @@ # source "$(dirname "$0")/get-script-header.sh" +GLPK_DIR="$DEPS_DIR/glpk-cut-log" commit=b420454e732f4b3d229c552ef7cd46fec75fe65c -if [ -e glpk-cut-log ]; then - echo 'error: file or directory "glpk-cut-log" exists; please move it out of the way.' >&2 - exit 1 -fi - -mkdir glpk-cut-log -cd glpk-cut-log -webget https://github.com/timothy-king/glpk-cut-log/archive/$commit.zip glpk-cut-log-$commit.zip -unzip glpk-cut-log-$commit.zip -cd glpk-cut-log-$commit +check_dep_dir "$GLPK_DIR" +setup_dep \ + "https://github.com/timothy-king/glpk-cut-log/archive/$commit.tar.gz" \ + "$GLPK_DIR" +cd "$GLPK_DIR" libtoolize aclocal autoheader autoconf automake --add-missing -./configure --without-pic --prefix=`pwd`/.. --disable-shared --enable-static --disable-dependency-tracking -make && make install -mv `pwd`/../lib/libglpk.a `pwd`/../lib/libglpk-static.a + +./configure --without-pic --prefix="$INSTALL_DIR" --disable-shared --enable-static --disable-dependency-tracking +make install -j$(nproc) make distclean -./configure --with-pic --prefix=`pwd`/.. --disable-shared --enable-static --disable-dependency-tracking -make && make install +mv "$INSTALL_LIB_DIR/libglpk.a" "$INSTALL_LIB_DIR/libglpk-static.a" -cd .. +./configure --with-pic --prefix="$INSTALL_DIR" --disable-shared --enable-static --disable-dependency-tracking +make install -j$(nproc) echo echo ===================== Now configure CVC4 with ===================== diff --git a/contrib/get-gmp b/contrib/get-gmp index aec125185..678103cf4 100755 --- a/contrib/get-gmp +++ b/contrib/get-gmp @@ -15,21 +15,21 @@ source "$(dirname "$0")/get-script-header.sh" [ -n "$HOST" ] && HOST="--host=$HOST" [ -z "$GMPVERSION" ] && GMPVERSION=6.1.2 +GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION" + +check_dep_dir "$GMP_DIR" + echo ============================================================================= echo echo "Setting up GMP $GMPVERSION..." echo -( set -ex - mkdir gmp-$GMPVERSION - cd gmp-$GMPVERSION - gmpprefix=`pwd` && - mkdir src && - cd src && - webget https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2 gmp-$GMPVERSION.tar.bz2 && - tar xfj gmp-$GMPVERSION.tar.bz2 && - cd gmp-$GMPVERSION && - ./configure ${HOST} --prefix="$gmpprefix" --enable-cxx ${BUILD_TYPE} && - make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" && - make install -) || exit 1 +setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR" +cd "$GMP_DIR" +./configure ${HOST} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE} +make \ + CFLAGS="${MAKE_CFLAGS}" \ + CXXFLAGS="${MAKE_CXXFLAGS}" \ + LDFLAGS="${MAKE_LDFLAGS}" \ + -j$(nproc) +make install echo diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker index 953d05d18..e7bee86c0 100755 --- a/contrib/get-lfsc-checker +++ b/contrib/get-lfsc-checker @@ -2,36 +2,17 @@ # source "$(dirname "$0")/get-script-header.sh" -lfscrepo="https://github.com/CVC4/LFSC.git" -dirname="lfsc-checker" +LFSC_DIR="$DEPS_DIR/lfsc-checker" +version="master" -function gitclone { - if [ -x "$(command -v git)" ] - then - git clone "$1" "$2" - else - echo "Need git to clone LFSC checker. Please install git." >&2 - exit 1 - fi -} +check_dep_dir "$LFSC_DIR" +setup_dep "https://github.com/CVC4/LFSC/archive/$version.tar.gz" "$LFSC_DIR" +cd "$LFSC_DIR" -if [ -e lfsc-checker ]; then - echo 'error: file or directory "lfsc-checker" already exists!' >&2 - exit 1 -fi - -mkdir $dirname -cd $dirname - -LFSC_PATH=`pwd` - -gitclone $lfscrepo . -mkdir install mkdir build cd build -cmake -DCMAKE_INSTALL_PREFIX:PATH=$LFSC_PATH/install .. -make install -cd .. +cmake -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" .. +make install -j$(nproc) echo echo ===================== Now configure CVC4 with ===================== diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh index 4e2a133b3..7a88b3be2 100644 --- a/contrib/get-script-header.sh +++ b/contrib/get-script-header.sh @@ -2,7 +2,15 @@ # set -e -o pipefail -cd "$(dirname "$0")/.." +[ ! -d contrib ] && echo "$0 not called from base directory" && exit 1 + +DEPS_DIR="$(pwd)/deps" +INSTALL_DIR="$DEPS_DIR/install" +INSTALL_LIB_DIR="$INSTALL_DIR/lib" +INSTALL_INCLUDE_DIR="$INSTALL_DIR/include" +INSTALL_BIN_DIR="$INSTALL_DIR/bin" + +mkdir -p "$DEPS_DIR" if ! [ -e src/parser/cvc/Cvc.g ]; then echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 @@ -36,3 +44,52 @@ if [ -z "$PYTHON" ]; then echo "Error: Couldn't find python, python2, or python3." >&2 exit 1 fi + +function setup_dep +{ + url="$1" + directory="$2" + echo "Setting up $directory ..." + mkdir -p "$directory" + cd "$directory" + webget "$url" archive + tar xf archive --strip 1 # Strip top-most directory + rm archive +} + +function check_dep_dir +{ + if [ -e "$1" ]; then + echo "error: file or directory '$1' exists; please move it out of the way." >&2 + exit 1 + fi +} + + +# Some of our dependencies do not provide a make install rule. Use the +# following helper functions to copy libraries/headers/binaries into the +# corresponding directories in deps/install. + +function install_lib +{ + echo "Copying $1 to $INSTALL_LIB_DIR" + [ ! -d "$INSTALL_LIB_DIR" ] && mkdir -p "$INSTALL_LIB_DIR" + cp "$1" "$INSTALL_LIB_DIR" +} + +function install_includes +{ + include="$1" + subdir="$2" + echo "Copying $1 to $INSTALL_INCLUDE_DIR/$subdir" + [ ! -d "$INSTALL_INCLUDE_DIR" ] && mkdir -p "$INSTALL_INCLUDE_DIR" + [ -n "$subdir" ] && [ ! -d "$INSTALL_INCLUDE_DIR/$subdir" ] && mkdir -p "$INSTALL_INCLUDE_DIR/$subdir" + cp -r "$include" "$INSTALL_INCLUDE_DIR/$subdir" +} + +function install_bin +{ + echo "Copying $1 to $INSTALL_BIN_DIR" + [ ! -d "$INSTALL_BIN_DIR" ] && mkdir -p "$INSTALL_BIN_DIR" + cp "$1" "$INSTALL_BIN_DIR" +} diff --git a/contrib/get-symfpu b/contrib/get-symfpu index b17c00299..885bad62e 100755 --- a/contrib/get-symfpu +++ b/contrib/get-symfpu @@ -2,20 +2,15 @@ # source "$(dirname "$0")/get-script-header.sh" -wdir="symfpu-CVC4" - -if [ -e $wdir ]; then - echo "error: file or directory "$wdir" exists; please move it out of the way." >&2 - exit 1 -fi - +SYMFPU_DIR="$DEPS_DIR/symfpu-CVC4" commit="8fbe139bf0071cbe0758d2f6690a546c69ff0053" -mkdir $wdir -cd $wdir -git clone https://github.com/martin-cs/symfpu.git symfpu -cd symfpu -git checkout $commit +check_dep_dir "$SYMFPU_DIR" +setup_dep \ + "https://github.com/martin-cs/symfpu/archive/$commit.tar.gz" "$SYMFPU_DIR" +cd "$SYMFPU_DIR" +install_includes core symfpu +install_includes utils symfpu echo echo "Using symfpu commit $commit"