on: [push, pull_request]
name: CI

jobs:
  build:
    strategy:
      matrix:
        include:
          - name: ubuntu:production
            os: ubuntu-latest
            config: production --auto-download --all-bindings --editline --docs
            cache-key: production
            python-bindings: true
            build-documentation: true
            check-examples: true
            exclude_regress: 3-4
            run_regression_args: --no-check-unsat-cores --no-check-proofs

          - name: macos:production
            os: macos-latest
            config: production --auto-download --all-bindings --editline
            cache-key: production
            python-bindings: true
            check-examples: true
            exclude_regress: 3-4
            run_regression_args: --no-check-unsat-cores --no-check-proofs

          - name: ubuntu:production-clang
            os: ubuntu-latest
            env: CC=clang CXX=clang++
            config: production --auto-download
            cache-key: productionclang
            check-examples: true
            exclude_regress: 3-4
            run_regression_args: --no-check-unsat-cores --no-check-proofs

          - name: ubuntu:production-dbg
            os: ubuntu-latest
            config: production --auto-download --assertions --tracing --unit-testing --editline
            cache-key: dbg
            exclude_regress: 3-4
            run_regression_args: --no-check-unsat-cores

          - name: ubuntu:production-dbg-clang
            os: ubuntu-latest
            env: CC=clang CXX=clang++
            config: production --auto-download --assertions --tracing --cln --gpl
            cache-key: dbgclang
            exclude_regress: 3-4
            run_regression_args: --no-check-proofs

    name: ${{ 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 \
          build-essential \
          ccache \
          libcln-dev \
          libgmp-dev \
          libgtest-dev \
          libedit-dev \
          flex \
          libfl-dev \
          flexc++
        python3 -m pip install toml
        python3 -m pip install setuptools
        python3 -m pip install pexpect
        cd /usr/src/googletest
        sudo cmake .
        sudo cmake --build . --target install
        cd -
        # Make ImageVersion accessible as env.image_version. Environment
        # variables of the runner are not automatically imported:
        #
        # https://github.com/actions/runner/blob/master/docs/adrs/0278-env-context.md#dont-populate-the-env-context-with-environment-variables-from-runner-machine
        echo "image_version=$ImageVersion" >> $GITHUB_ENV
        echo "/usr/lib/ccache" >> $GITHUB_PATH

    # Note: macOS comes with a libedit; it does not need to brew-installed
    - name: Install Packages (macOS)
      if: runner.os == 'macOS'
      run: |
        brew update
        brew install \
          ccache \
          cln \
          gmp \
          pkgconfig \
          flex
        python3 -m pip install toml
        python3 -m pip install setuptools
        python3 -m pip install pexpect
        # Make ImageVersion accessible as env.image_version. Environment
        # variables of the runner are not automatically imported:
        #
        # https://github.com/actions/runner/blob/master/docs/adrs/0278-env-context.md#dont-populate-the-env-context-with-environment-variables-from-runner-machine
        echo "image_version=$ImageVersion" >> $GITHUB_ENV
        echo "/usr/local/opt/ccache/libexec" >> $GITHUB_PATH

    - name: Install Python Dependencies
      if: matrix.python-bindings
      run: |
        python3 -m pip install pytest
        python3 -m pytest --version
        python3 -m pip install scikit-build
        python3 -m pip install \
          Cython==0.29.* --install-option="--no-cython-compile"
        echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH
    
    - name: Install Documentation Dependencies
      if: matrix.build-documentation
      run: |
        sudo apt-get install -y doxygen python3-docutils python3-jinja2
        python3 -m pip install \
          sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme breathe

    # The GitHub action for caching currently does not support modifying an
    # already existing cache. We thus have a few different possibilities:
    # - If having (partially) outdated data in the cached directory is fine, we
    #   may want to restore any old cache via `restore-keys`. We should try hard
    #   to detect that we have (partially) outdated data and make sure that the
    #   updated data is stored to a new cache key.
    # - If a cache is updated frequently (i.e. almost with every commit), we
    #   should use the current commit hash as suffix and use `restore-keys` to
    #   restore the cache from the previous commit.
    #
    # We define three caches: aux-tools, ccache, deps.
    # - aux-tools (deps/) does not handle outdated contents gracefully. As it is
    #   not updated frequently, we completely rebuild it whenever it might
    #   change, which is when the contrib scripts or the CI config changes.
    # - ccache changes with (almost) every commit and handles outdated contents
    #   properly. We thus use `restore-keys` and store a new cache for every
    #   commit.
    # - deps (build/deps/) does handle outdated contents gracefully, but does
    #   not change frequently. We thus use `restore-keys` to restore any recent
    #   cache, but only store a new cache if the cmake or CI config changes.
    #
    # All caches are separated by operating system. Both ccache and deps are
    # additionally separated by `cache-key`, i.e. the CI job type, because they
    # depend on the configured compiler.

    - name: Restore Auxiliary Tools
      id: restore-aux-tools
      uses: actions/cache@v2
      with:
        path: deps/install
        key: cvc5-aux-tools-${{ runner.os }}-${{ hashFiles('contrib/get-**') }}-${{ hashFiles('.github/workflows/ci.yml') }}

    - name: Setup Auxiliary Tools
      if: steps.restore-aux-tools.outputs.cache-hit != 'true'
      run: |
        ./contrib/get-lfsc-checker

    - name: Restore ccache
      id: ccache
      uses: actions/cache@v2
      with:
        path: ccache-dir
        key: cvc5-ccache-${{ runner.os }}-${{ matrix.cache-key }}-${{ github.sha }}
        restore-keys: cvc5-ccache-${{ 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: Restore Dependencies
      id: restore-deps
      uses: actions/cache@v2
      with:
        path: build/deps
        # The cache depends on the image version to make sure that we do not
        # restore the dependencies if the build environment has changed.
        key: cvc5-deps-${{ runner.os }}-${{ env.image_version }}-${{ matrix.cache-key }}-${{ hashFiles('cmake/Find**', 'cmake/deps-helper.cmake') }}-${{ hashFiles('.github/workflows/ci.yml') }}

    - name: Configure
      run: |
        ${{ matrix.env }} ./configure.sh ${{ matrix.config }} \
          --prefix=$(pwd)/build/install \
          --werror

    - 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[${{ matrix.exclude_regress }}]
        CVC5_REGRESSION_ARGS: --no-early-exit
        RUN_REGRESSION_ARGS: ${{ matrix.run_regression_args }}
      working-directory: build

    - name: Install Check
      run: |
        make -j2 install
        echo -e "#include <cvc5/cvc5.h>\nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp
        g++ -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc5
      working-directory: build

    - name: Python Install Check
      if: matrix.python-bindings
      run: |
       export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc5" -type d))"
       python3 -c "import pycvc5"

      # 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

    - name: Build Documentation
      if: matrix.build-documentation
      run: |
        make -j2 docs-gh
        if [ "${{ github.event_name }}" == "pull_request" ] ; then
          echo "${{ github.event.number }}" > docs/sphinx-gh/prnum
        fi
      working-directory: build
    
    - name: Store Documentation
      if: matrix.build-documentation
      uses: actions/upload-artifact@v2
      with:
        name: documentation
        path: build/docs/sphinx-gh/