--- /dev/null
+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
+
+++ /dev/null
-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