Merge pull request #33 from pysmt/solvers_bin_mirror_clean

Binary mirrors for solvers: CUDD, CVC4 and Z3.

install.py

@@ -32,6 +32,8 @@
 # Address of a mirror website containing packages to avoid continuous
 # downloads from original websites in CI
 mirror = os.environ.get('PYSMT_INSTALL_MIRROR')
+# Download a binary version of the compiled solver (Used by CI)
+bin_mirror = os.environ.get('PYSMT_BIN_MIRROR')
 
 
 ################################################################################
@@ -165,11 +167,19 @@ def install_z3(options):
     dir_path = os.path.join(BASE_DIR, base_name)
     install_path = os.path.join(BASE_DIR, "z3_bin")
 
+    # Use precompiled version of the solver
+    if bin_mirror is not None:
+        bin_archive = os.path.join(bin_mirror, archive_name)
+        download(bin_archive, archive)
+        unzip(archive, install_path)
+        PATHS.append("%s/lib/python2.7/dist-packages" % install_path)
+        return
+
     # Download the z3 release if needed
     if not os.path.exists(archive):
         download(get_z3_download_link(git), archive)
 
-    # clear the destination directory, if any
+    # Clear the destination directory, if any
     if os.path.exists(dir_path):
         os.system("rm -rf %s" % dir_path)
 
@@ -200,6 +210,15 @@ def install_cvc4(options):
     archive = os.path.join(BASE_DIR, archive_name)
     dir_path = os.path.join(BASE_DIR, base_name)
 
+    # Use precompiled version of the solver
+    if bin_mirror is not None:
+        bin_archive = os.path.join(bin_mirror, archive_name)
+        download(bin_archive, archive)
+        untar(archive, BASE_DIR)
+        PATHS.append("%s/CVC4_bin/share/pyshared" % BASE_DIR)
+        PATHS.append("%s/CVC4_bin/lib/pyshared" % BASE_DIR)
+        return
+
     # Download the cvc4 release if needed
     if not os.path.exists(archive):
         download(get_cvc4_download_link(git), archive)
@@ -221,8 +240,8 @@ def install_cvc4(options):
     # Configure and build CVC4
     os.system("cd %s; \
     ./configure --enable-language-bindings=python \
-                --with-antlr-dir=%s/antlr-3.4 ANTLR=%s/antlr-3.4/bin/antlr3;\
-    make -j%d" % (dir_path, dir_path, dir_path, options.make_j))
+                --with-antlr-dir=%s/antlr-3.4 ANTLR=%s/antlr-3.4/bin/antlr3; make " %\
+              (dir_path, dir_path, dir_path))
     # Fix the paths of the bindings
     os.system("cd %s/builds/src/bindings/python; mv .libs/CVC4.so.3.0.0 ./_CVC4.so" % dir_path)
 
@@ -294,6 +313,14 @@ def install_pycudd(options):
     archive = os.path.join(BASE_DIR, archive_name)
     dir_path = os.path.join(BASE_DIR, base_name)
 
+    # Use precompiled version of the solver
+    if bin_mirror is not None:
+        bin_archive = os.path.join(bin_mirror, archive_name)
+        download(bin_archive, archive)
+        untar(archive, BASE_DIR)
+        PATHS.append("%s/lib/python2.7/dist-packages" % dir_path)
+        return
+
     # Download pycudd if needed
     if not os.path.exists(archive):
         download(get_pycudd_download_link(archive_name), archive)

shippable.sh

@@ -35,7 +35,7 @@ fi
 if [ "$1" == "cudd" ]
 then
     apt-get update
-    apt-get install -y make build-essential swig libgmp-dev
+    apt-get install -y make build-essential swig
     apt-get install -y python-all-dev
     ./install.py --confirm-agreement --cudd  --make-j 2
 fi

shippable.yml

@@ -1,14 +1,8 @@
-cache: true
+# cache: true # This yields random results
 language: python
 build_image: shippableimages/ubuntu1404_python
 python:
-  # - 2.6
   - 2.7
-  # - 3.2
-  # - 3.3
-  # - 3.4
-  # - pypy
-
 
 install:
   - pip install nose
@@ -23,12 +17,14 @@ install:
 #
 env:
   global:
+    # These variables are used to set mirrors for the solvers
     - secure: IzzUEuWb2+h3gzttT0237NDkptzu4UvPN1okinDgm4Rx0uADXVWJy6gvcWaeL8F6tl8KGkpcFvzGHmwj7RGGRk8AAj+OVf+VilSlWwNe1g8SYHwxOPrTgD4ECX3860hleeI3F2DD+yFIo9Hgw3ZiHBsfbombtFGTB5WWwUgezXsENMKuNJ580MN8+c3I4IV44pSXJ179GluJ3O1e/xUkwJ5/nvysWd4q7wqJ6aIz5ZFMFhs/FKAbeEdtmmGODn2FspGJ+iKVyc0IbQpzLJO1MeizBXnGZfN9Ojv7mkPJcgzqFMjvLnpCJAEmZl3BzJFc0j9xxILvrrjHU/TKrlJkSw==
+    - secure: nuGI4WDZOFDezaSxQUKyOP19iqRmQSASv5tpCCsryQ3AtI3in/1dYndDUwmzGYfoVkHTOsf6n4O3XEAruktPpVZzLSlek9zcr8v0IERTfzhoGCWRqqYDrDoCU6Hc2WYyGOhGGEzfldsY1EVMx5+LsVz0JoVZFe75CO6oWvuEYVYRmeJYzKQWLuXXwQMkfYulX1ouF1b5JCdeepbUfwcf4o34RPrd6eLoL7Y1RT4SBsR0uX4lpnWvUB2qqoyOEvu/hXt9Zft57tW4OY2GUdlRlj/Hx/5fPIFGYJmsGu7BM/+Q1cLgZnyyH0mxaHtBkjt8ecMwUc/9PbNJ2alZDmIMyw==
   matrix:
-    - PYSMT_SOLVER="None"
     - PYSMT_SOLVER="msat"  PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/mathsat-5.2.12-linux-x86_64/python:$TRAVIS_BUILD_DIR/.smt_solvers/mathsat-5.2.12-linux-x86_64/python/build/lib.linux-x86_64-2.7"
     - PYSMT_SOLVER="z3"    PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/z3_bin/lib/python2.7/dist-packages"
-    - PYSMT_SOLVER="cvc4"  PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/CVC4-68f22235a62f5276b206e9a6692a85001beb8d42/builds/src/bindings/python"
+    # We use a different path for binary CVC4 to keep the pkg that we need to download small
+    - PYSMT_SOLVER="cvc4"  PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/CVC4_bin/share/pyshared:$TRAVIS_BUILD_DIR/.smt_solvers/CVC4_bin/lib/pyshared"
     - PYSMT_SOLVER="yices" PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/pyices-aa0b91c39aa00c19c2160e83aad822dc468ce328/build/lib.linux-x86_64-2.7"
     - PYSMT_SOLVER="cudd"  PYTHONPATH="$PYTHONPATH:$TRAVIS_BUILD_DIR/.smt_solvers/pycudd2.0.2/pycudd"
 
@@ -52,7 +48,5 @@ script:
   - ./install.py --check
   - nosetests pysmt --processes=4 --process-timeout=360 --with-xunit --xunit-file=shippable/testresults/nosetests.xml
 
-# --with-coverage --cover-package=pysmt --cover-xml --cover-xml-file=shippable/codecoverage/coverage.xml --cover-branch
-
-# Disable push of container for now
-#commit_container: gario/shippable_pysmt
+# Push of container is disabled
+# commit_container: gario/shippable_pysmt