Switch to GitHub actions for CI (#4190)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 31 Mar 2020 23:44:03 +0000 (16:44 -0700)
committerGitHub <noreply@github.com>
Tue, 31 Mar 2020 23:44:03 +0000 (16:44 -0700)
Enable CI with GitHub actions, add macOS builds and disable Travis CI.

.github/workflows/ci.yml [new file with mode: 0644]
.travis.yml [deleted file]
README.md
configure.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644 (file)
index 0000000..99654b7
--- /dev/null
@@ -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 (file)
index 8297813..0000000
+++ /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
index 53398e00b8b1e9f80a9e4723930575a8a120c2ef..e2318ec55dcdad722022db900a3e321317a885b5 100644 (file)
--- a/README.md
+++ b/README.md
@@ -1,9 +1,7 @@
 [![License: BSD](
     https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](
         https://opensource.org/licenses/BSD-3-Clause)
-[![Build Status](
-    https://travis-ci.org/CVC4/CVC4.svg?branch=master)](
-        https://travis-ci.org/CVC4/CVC4)
+![CI](https://github.com/CVC4/CVC4/workflows/CI/badge.svg)
 [![Coverage](
   https://img.shields.io/endpoint?url=https://cvc4.cs.stanford.edu/downloads/builds/coverage/nightly-coverage.json)](
     https://cvc4.cs.stanford.edu/downloads/builds/coverage)
index bd95e38ed7a547bedf6c2e250309e88814551cc7..070e2c23025762cab92f67652325f1655c1a6c76 100755 (executable)
@@ -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')