Add CI workflow to test different cmake versions (#7254)

This refactors the CI setup by moving parts of the CI workflow into new composite actions. This allows to reuse this parts in a new workflow that tests against many different cmake versions. It is mostly useful after modifying our cmake setup to check compatibility with older cmake versions.
The workflow is not triggered automatically, but can be started manually.

4 files changed, 220 insertions, 0 deletions

diff --git a/.github/actions/build-documentation/action.yml b/.github/actions/build-documentation/action.yml
new file mode 100644
index 000000000..cb5587c51
--- /dev/null
+++ b/.github/actions/build-documentation/action.yml
@@ -0,0 +1,19 @@
+name: Build documentation
+description: Build documentation and store it as artifact
+runs:
+  using: composite
+  steps:
+    - name: Build Documentation
+      shell: bash
+      run: |
+        make -j${{ env.num_proc }} docs-gh
+        if [ "${{ github.event_name }}" == "pull_request" ] ; then
+          echo "${{ github.event.number }}" > docs/sphinx-gh/prnum
+        fi
+      working-directory: build
+    
+    - name: Store Documentation
+      uses: actions/upload-artifact@v2
+      with:
+        name: documentation
+        path: build/docs/sphinx-gh/
diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml
new file mode 100644
index 000000000..254354de3
--- /dev/null
+++ b/.github/actions/install-dependencies/action.yml
@@ -0,0 +1,78 @@
+name: Install dependencies
+description: Install necessary dependencies on the target system
+inputs:
+  with-documentation:
+    default: false
+  with-python-bindings:
+    default: false
+runs:
+  using: composite
+  steps:
+    - name: Install Linux software
+      shell: bash
+      run: |
+        if [[ $RUNNER_OS != "Linux" ]]; then exit 0; fi
+        sudo apt-get update
+        sudo apt-get install -y \
+          build-essential \
+          ccache \
+          libbsd-dev \
+          libcln-dev \
+          libedit-dev \
+          libgmp-dev \
+          libgtest-dev \
+          libtinfo-dev \
+          flex \
+          libfl-dev \
+          flexc++
+        python3 -m pip install pexpect setuptools toml
+        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 "num_proc=$(nproc)" >> $GITHUB_ENV
+        echo "/usr/lib/ccache" >> $GITHUB_PATH
+
+    # Note: macOS comes with a libedit; it does not need to brew-installed
+    - name: Install macOS software
+      shell: bash
+      run: |
+        if [[ $RUNNER_OS != "macOS" ]]; then exit 0; fi
+        brew update --quiet
+        brew install \
+          ccache \
+          cln \
+          gmp \
+          pkgconfig \
+          flex
+        python3 -m pip install pexpect setuptools toml
+        # 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 "num_proc=$(sysctl -n hw.logicalcpu)" >> $GITHUB_ENV
+        echo "/usr/local/opt/ccache/libexec" >> $GITHUB_PATH
+
+    - name: Install Python packages
+      shell: bash
+      run: |
+        if [[ "${{ inputs.with-python-bindings }}" != "true" ]]; then exit 0; fi
+        python3 -m pip install pytest scikit-build
+        python3 -m pytest --version
+        python3 -m pip install \
+          Cython==0.29.* --install-option="--no-cython-compile"
+        echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH
+    
+    - name: Install software for documentation
+      shell: bash
+      run: |
+        if [[ "${{ inputs.with-documentation }}" != "true" ]]; then exit 0; fi
+        sudo apt-get install -y doxygen python3-docutils python3-jinja2
+        python3 -m pip install \
+          sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme breathe
diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml
new file mode 100644
index 000000000..e5557bb2d
--- /dev/null
+++ b/.github/actions/run-tests/action.yml
@@ -0,0 +1,54 @@
+name: Run tests
+description: Run all available tests
+inputs:
+  check-examples:
+    default: true
+  check-python-bindings:
+    default: false
+  check-unit-tests:
+    default: true
+runs:
+  using: composite
+  steps:
+    - name: Run CTest
+      shell: bash
+      run: |
+        make -j${{ env.num_proc }} 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: Run Unit Tests
+      shell: bash
+      run: |
+        if [[ "${{ inputs.check-unit-tests }}" != "true" ]]; then exit 0; fi
+        make -j${{ env.num_proc }} apitests units
+      working-directory: build
+
+    - name: Install Check
+      shell: bash
+      run: |
+        make -j${{ env.num_proc }} install
+        echo -e "#include <cvc5/cvc5.h>\nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp
+        g++ -std=c++17 /tmp/test.cpp -I install/include -L install/lib -lcvc5
+      working-directory: build
+
+    - name: Python Install Check
+      shell: bash
+      run: |
+        if [[ "${{ inputs.check-python-bindings }}" != "true" ]]; then exit 0; fi
+        export PYTHONPATH="$PYTHONPATH:$(dirname $(find build/install/ -name "pycvc5" -type d))"
+        python3 -c "import pycvc5"
+
+    - name: Check Examples
+      shell: bash
+      run: |
+        if [[ "${{ inputs.check-examples }}" != "true" ]]; then exit 0; fi
+        mkdir build
+        cd build
+        cmake .. -DCMAKE_PREFIX_PATH=$(pwd)/../../build/install/lib/cmake
+        make -j${{ env.num_proc }}
+        ctest -j${{ env.num_proc }} --output-on-failure
+      working-directory: examples
\ No newline at end of file
diff --git a/.github/actions/setup-cache/action.yml b/.github/actions/setup-cache/action.yml
new file mode 100644
index 000000000..ad485f2dc
--- /dev/null
+++ b/.github/actions/setup-cache/action.yml
@@ -0,0 +1,69 @@
+name: Setup cache
+description: Setup caches (ccache, contribs and dependencies)
+inputs:
+  cache-key:
+    default: "none"
+
+# 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: ccache, contrib and deps.
+# - ccache changes with (almost) every commit and handles outdated contents
+#   properly. We thus use `restore-keys` and store a new cache for every
+#   commit.
+# - contrib (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.
+# - 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.
+
+runs:
+  using: composite
+  steps:
+    - name: Setup ccache cache
+      uses: actions/cache@v2
+      with:
+        path: ccache-dir
+        key: ${{ inputs.cache-key }}-${{ runner.os }}-ccache-${{ github.sha }}
+        restore-keys: ${{ inputs.cache-key }}-${{ runner.os }}-ccache-
+
+    - name: Configure ccache
+      shell: bash
+      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: Setup contrib dependencies cache
+      id: contrib-cache
+      uses: actions/cache@v2
+      with:
+        path: deps/install
+        key: ${{ inputs.cache-key }}-${{ runner.os }}-contrib-${{ hashFiles('contrib/get-**') }}-${{ hashFiles('.github/**') }}
+
+    - name: Install contrib dependencies
+      shell: bash
+      run: |
+        if [[ "${{ steps.contrib-cache.outputs.cache-hit }}" == "true" ]]; then exit 0; fi
+        ./contrib/get-lfsc-checker
+
+    - name: Setup dependencies cache
+      uses: actions/cache@v2
+      with:
+        path: build/deps
+        key: ${{ inputs.cache-key }}-${{ runner.os }}-deps-${{ hashFiles('cmake/**') }}-${{ hashFiles('.github/**') }}
+