diff options
| -rw-r--r-- | .github/workflows/ci.yml | 168 | ||||
| -rw-r--r-- | .travis.yml | 153 | ||||
| -rw-r--r-- | README.md | 4 | ||||
| -rwxr-xr-x | configure.sh | 6 |
4 files changed, 173 insertions, 158 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 000000000..99654b794 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,168 @@ +on: [push, pull_request] +name: CI + +jobs: + build: + + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + name: [ + production, + production-clang, + debug, + debug-cln + ] + + include: + - name: production + config: production --language-bindings=java --lfsc --python-bindings + cache-key: production + python-bindings: true + check-examples: true + + - name: production-clang + config: production + cache-key: production-clang + check-examples: true + env: CC=clang CXX=clang++ + + - name: debug + config: debug --symfpu --lfsc --no-debug-symbols + cache-key: debug + + - name: debug-cln + config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs + cache-key: debug-cln + + name: ${{ matrix.os }}:${{ matrix.name }} + runs-on: ${{ matrix.os }} + + steps: + + - uses: actions/checkout@v2 + + - name: Install Packages + if: runner.os == 'Linux' + run: | + sudo apt-get update + sudo apt-get install -y \ + ccache \ + cxxtest \ + libcln-dev \ + libgmp-dev \ + swig3.0 + python3 -m pip install toml + python3 -m pip install setuptools + echo "::add-path::/usr/lib/ccache" + + - name: Install Packages (macOS) + if: runner.os == 'macOS' + run: | + brew install \ + ccache \ + cxxtest \ + cln \ + gmp \ + swig + python3 -m pip install toml + python3 -m pip install setuptools + echo "::add-path::/usr/local/opt/ccache/libexec" + + # Note: We install Cython with sudo since cmake can't find Cython otherwise. + - name: Install Cython + if: matrix.python-bindings && runner.os == 'Linux' + run: | + sudo python3 -m pip install \ + Cython==0.29 --install-option="--no-cython-compile" + + - name: Install Cython (macOS) + if: matrix.python-bindings && runner.os == 'macOS' + run: | + python3 -m pip install \ + Cython==0.29 --install-option="--no-cython-compile" + + - name: Restore Dependencies + id: restore-deps + uses: actions/cache@v1 + with: + path: deps/install + key: ${{ runner.os }}-deps-${{ hashFiles('contrib/get-**.sh') }}-${{ hashFiles('.github/workflows/ci.yml') }} + + - name: Setup Dependencies + if: steps.restore-deps.outputs.cache-hit != 'true' + run: | + ./contrib/get-antlr-3.4 + ./contrib/get-symfpu + ./contrib/get-cadical + ./contrib/get-cryptominisat + ./contrib/get-lfsc-checker + + # GitHub actions currently does not support modifying an already existing + # cache. Hence, we create a new cache for each commit with key + # cache-${{ runner.os }}-${{ matrix.cache-key }}-${{ github.sha }}. This + # will result in an initial cache miss. However, restore-keys will search + # for the most recent cache with prefix + # cache-${{ runner.os }}-${{ matrix.cache-key }}-, and if found uses it as + # a base for the new cache. + - name: Restore ccache + id: cache + uses: actions/cache@v1 + with: + path: ccache-dir + key: cache-${{ runner.os }}-${{ matrix.cache-key }}-${{ github.sha }} + restore-keys: cache-${{ runner.os }}-${{ matrix.cache-key }}- + + - name: Configure ccache + run: | + ccache --set-config=cache_dir=${{ github.workspace }}/ccache-dir + ccache --set-config=compression=true + ccache --set-config=compression_level=6 + ccache -M 500M + ccache -z + + - name: Configure + run: | + ${{ matrix.env }} ./configure.sh ${{ matrix.config }} \ + --python3 \ + --prefix=$(pwd)/build/install \ + --unit-testing + + - name: Build + run: make -j2 + working-directory: build + + - name: ccache Statistics + run: ccache -s + + - name: Run CTest + run: make -j2 check + env: + ARGS: --output-on-failure -LE regress[1-4] + CVC4_REGRESSION_ARGS: --no-early-exit + working-directory: build + + - name: Install Check + run: | + make -j2 install + echo -e "#include <cvc4/api/cvc4cpp.h>\nint main() { CVC4::api::Solver s; return 0; }" > /tmp/test.cpp + g++ -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc4 + working-directory: build + + - name: Python Install Check + if: matrix.python-bindings + run: | + export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc4" -type d))" + python3 -c "import pycvc4" + + # Examples are built for non-symfpu builds + - name: Check Examples + if: matrix.check-examples && runner.os == 'Linux' + run: | + mkdir build + cd build + cmake .. -DCMAKE_PREFIX_PATH=$(pwd)/../../build/install/lib/cmake + make -j2 + ctest -j2 --output-on-failure + working-directory: examples + diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 8297813da..000000000 --- a/.travis.yml +++ /dev/null @@ -1,153 +0,0 @@ -language: cpp -cache: - - apt - - ccache - -sudo: false -dist: xenial - -env: - global: - - CCACHE_COMPRESS=1 -addons: - apt: - sources: - - ubuntu-toolchain-r-test - packages: &common_deps - - antlr3 - - cmake - - cxxtest - - junit4 - - libantlr3c-dev - - libcln-dev - - libgmp-dev - - libhamcrest-java - - openjdk-8-jdk - - python3 - - python3-pip - - python3-setuptools - - swig3.0 -before_install: - # Clang does not play nice with ccache (at least the versions offered by - # Travis), use a workaround: - # https://github.com/travis-ci/travis-ci/issues/5383#issuecomment-224630584 - - | - if [ "$TRAVIS_OS_NAME" == "linux" ] && [ "$CXX" == "clang++" ]; then - export CFLAGS="-Qunused-arguments" - export CXXFLAGS="-Qunused-arguments" - sudo ln -s $(which ccache) /usr/lib/ccache/clang - sudo ln -s $(which ccache) /usr/lib/ccache/clang++ - fi -before_script: - export JAVA_HOME=/usr/lib/jvm/java-8-openjdk-amd64 -script: - - ccache -M 1G - - ccache -z - - ${CC} --version - - ${CXX} --version - - sudo ${TRAVIS_PYTHON} -m pip install toml - - sudo ${TRAVIS_PYTHON} -m pip install Cython==0.29 --install-option="--no-cython-compile" - - | - echo "travis_fold:start:load_script" - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')" - configureCVC4() { - echo "CVC4 config - $TRAVIS_CVC4_CONFIG"; - ./configure.sh --name=build --prefix=$(pwd)/build/install --unit-testing $TRAVIS_CVC4_CONFIG - } - error() { - echo; - echo "${red}${1}${normal}"; - echo; - exit 1; - } - makeCheck() { - ( - cd build - make -j2 check ARGS='-LE regress[1-4]' CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED" - ) - } - makeExamples() { - ( - cd examples - mkdir build - cd build - cmake .. -DCMAKE_PREFIX_PATH=$(pwd)/../../build/install/lib/cmake - make -j2 - ctest -j2 --output-on-failure || error "RUNNING EXAMPLES FAILED" - ) - } - makeInstallCheck() { - ( - cd build - make install -j2 - echo -e "#include <cvc4/cvc4.h>\nint main() { CVC4::ExprManager em; return 0; }" > /tmp/test.cpp - $CXX -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc4 -lcln || exit 1 - # set PYTHONPATH to include the directory containing pycvc4 module - export PYTHONPATH=$PYTHONPATH:$(dirname $(find ./install/ -name "pycvc4" -type d)) - if [[ "$TRAVIS_CVC4_PYTHON_BINDINGS" == "yes" ]]; then - $TRAVIS_PYTHON -c "import pycvc4" || exit 1 - fi - ) - } - run() { - echo "travis_fold:start:$1" - echo "Running $1" - $1 || exit 1 - echo "travis_fold:end:$1" - } - [[ "$TRAVIS_CVC4_CONFIG" == *"symfpu"* ]] && CVC4_SYMFPU_BUILD="yes" - [ -n "$CVC4_SYMFPU_BUILD" ] && run contrib/get-symfpu - [ -n "$TRAVIS_CVC4" ] && [ -n "$TRAVIS_WITH_LFSC" ] && run contrib/get-lfsc-checker - [ -n "$TRAVIS_CVC4" ] && run configureCVC4 - [ -n "$TRAVIS_CVC4" ] && run makeCheck - [ -z "$CVC4_SYMFPU_BUILD" ] && run makeInstallCheck && run makeExamples - [ -z "$TRAVIS_CVC4" ] && error "Unknown Travis-CI configuration" - echo "travis_fold:end:load_script" - - echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}" - - ccache -s -matrix: - fast_finish: true - include: - # Test with GCC - - compiler: gcc - env: - - TRAVIS_CVC4=yes - - TRAVIS_WITH_LFSC=yes - - TRAVIS_CVC4_PYTHON_BINDINGS=no - - TRAVIS_CVC4_CONFIG="production --language-bindings=java --lfsc" - - TRAVIS_PYTHON=python - - compiler: gcc - env: - - TRAVIS_CVC4=yes - - TRAVIS_WITH_LFSC=yes - - TRAVIS_CVC4_PYTHON_BINDINGS=no - - TRAVIS_CVC4_CONFIG="debug --symfpu --lfsc --no-debug-symbols" - - TRAVIS_PYTHON=python - # Test python bindings - - compiler: gcc - env: - - TRAVIS_CVC4=yes - - TRAVIS_WITH_LFSC=yes - - TRAVIS_CVC4_PYTHON_BINDINGS=yes - - TRAVIS_CVC4_CONFIG="production --python-bindings --python2" - - TRAVIS_PYTHON=python - - compiler: gcc - env: - - TRAVIS_CVC4=yes - - TRAVIS_WITH_LFSC=yes - - TRAVIS_CVC4_PYTHON_BINDINGS=yes - - TRAVIS_CVC4_CONFIG="production --python-bindings --python3" - - TRAVIS_PYTHON=python3 - # - # Test with Clang - - compiler: clang - env: - - TRAVIS_CVC4=yes - - TRAVIS_WITH_LFSC=yes - - TRAVIS_CVC4_PYTHON_BINDINGS=no - - TRAVIS_CVC4_CONFIG="debug --symfpu --cln --gpl --no-debug-symbols --no-proofs" - - TRAVIS_PYTHON=python -notifications: - email: - on_success: change - on_failure: always @@ -1,9 +1,7 @@ []( https://opensource.org/licenses/BSD-3-Clause) -[]( - https://travis-ci.org/CVC4/CVC4) + []( https://cvc4.cs.stanford.edu/downloads/builds/coverage) diff --git a/configure.sh b/configure.sh index bd95e38ed..070e2c230 100755 --- a/configure.sh +++ b/configure.sh @@ -1,6 +1,8 @@ -#!/bin/sh +#!/bin/bash #--------------------------------------------------------------------------# +set -e -o pipefail + usage () { cat <<EOF Usage: $0 [<build type>] [<option> ...] @@ -458,7 +460,7 @@ root_dir=$(pwd) [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir" mkdir -p "$build_dir" -cd "$build_dir" || exit 1 +cd "$build_dir" [ -e CMakeCache.txt ] && rm CMakeCache.txt build_dir_escaped=$(echo "$build_dir" | sed 's/\//\\\//g') |