contrib: Setup all dependencies in deps/ directory. (#3534)

10 files changed, 169 insertions, 158 deletions

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 <<EOF
+mkdir -p "$ANTLR_HOME_DIR/share/java"
+webget \
+  "https://www.antlr3.org/download/antlr-3.4-complete.jar" \
+  "$ANTLR_HOME_DIR/share/java/antlr-3.4-complete.jar"
+
+mkdir -p "$ANTLR_HOME_DIR/bin"
+tee "$ANTLR_HOME_DIR/bin/antlr3" <<EOF
 #!/usr/bin/env bash
-export CLASSPATH=`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH
+export CLASSPATH=$ANTLR_HOME_DIR/share/java/antlr-3.4-complete.jar:\$CLASSPATH
 exec java org.antlr.Tool "\$@"
 EOF
-chmod a+x bin/antlr3
-cd src
-gunzip -f libantlr3c-3.4.tar.gz
-tar xfv libantlr3c-3.4.tar
-cd libantlr3c-3.4
+chmod a+x "$ANTLR_HOME_DIR/bin/antlr3"
+install_bin "$ANTLR_HOME_DIR/bin/antlr3"
 
-# Use an absolute path for the installation directory to avoid spurious libtool
-# warnings about the ANTLR library having moved
-PREFIX=$($PYTHON -c "import os; print(os.path.realpath('$(pwd)/../..'))")
+setup_dep \
+  "https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz" \
+  "$ANTLR_HOME_DIR/libantlr3c-3.4"
+cd "$ANTLR_HOME_DIR/libantlr3c-3.4"
 
 # Make antlr3debughandlers.c empty to avoid unreferenced symbols
 rm -rf src/antlr3debughandlers.c && touch src/antlr3debughandlers.c
-if [ ${MACHINE_TYPE} == 'x86_64' ]; then
+if [ "${MACHINE_TYPE}" == 'x86_64' ]; then
   # 64-bit stuff here
-  ./configure --enable-64bit --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+  ./configure --enable-64bit --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 else
   # 32-bit stuff here
-  ./configure --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+  ./configure --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 fi
 
 cp Makefile Makefile.orig
@@ -67,35 +64,27 @@ if [[ $WINDOWS_BUILD == "yes" ]]; then
   exit 0
 fi
 
-cd ../..
-mv lib/libantlr3c.a lib/libantlr3c-static.a
-
-cd src/libantlr3c-3.4
+mv "$INSTALL_LIB_DIR/libantlr3c.a" "$INSTALL_LIB_DIR/libantlr3c-static.a"
 make clean
 
-if [ ${MACHINE_TYPE} == 'x86_64' ]; then
+if [ "${MACHINE_TYPE}" == 'x86_64' ]; then
   # 64-bit stuff here
-  ./configure --enable-64bit --with-pic --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+  ./configure --enable-64bit --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 else
   # 32-bit stuff here
-  ./configure --with-pic --disable-antlrdebug --prefix="${PREFIX}" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+  ./configure --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 fi
 
 cp Makefile Makefile.orig
 sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig > 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"