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.

6 files changed, 297 insertions, 178 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/**') }}
+
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index df59ad379..8d88cad49 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -59,137 +59,16 @@ jobs:
 
     - uses: actions/checkout@v2
 
-    - name: Install Packages
-      if: runner.os == 'Linux'
-      run: |
-        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 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 "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 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 "num_proc=$(sysctl -n hw.logicalcpu)" >> $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
+    - name: Install dependencies
+      uses: ./.github/actions/install-dependencies
       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
+        with-documentation: ${{ matrix.build-documentation }}
+        with-python-bindings: ${{ matrix.python-bindings }}
 
-    - name: Restore Dependencies
-      id: restore-deps
-      uses: actions/cache@v2
+    - name: Setup caches
+      uses: ./.github/actions/setup-cache
       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') }}
+        cache-key: ${{ matrix.cache-key }}
 
     - name: Configure
       run: |
@@ -204,58 +83,16 @@ jobs:
     - name: ccache Statistics
       run: ccache -s
 
-    - name: Run CTest
-      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
-      if: matrix.check-units
-      run: make -j${{ env.num_proc }} apitests units
-      working-directory: build
-
-    - name: Install Check
-      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
-      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 -j${{ env.num_proc }}
-        ctest -j${{ env.num_proc }} --output-on-failure
-      working-directory: examples
+    - name: Run tests
+      uses: ./.github/actions/run-tests
+      with:
+        check-examples: ${{ matrix.check-examples }}
+        check-python-bindings: ${{ matrix.python-bindings }}
+        check-unit-tests: ${{ matrix.check-units }}
 
-    - name: Build Documentation
+    - name: Build documentation
       if: matrix.build-documentation
-      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
-      if: matrix.build-documentation
-      uses: actions/upload-artifact@v2
-      with:
-        name: documentation
-        path: build/docs/sphinx-gh/
+      uses: ./.github/actions/build-documentation
 
     - name: Add binary to release
       if: matrix.store-to-release && startsWith(github.ref, 'refs/tags/')
diff --git a/.github/workflows/cmake-version.yml b/.github/workflows/cmake-version.yml
new file mode 100644
index 000000000..d61c59088
--- /dev/null
+++ b/.github/workflows/cmake-version.yml
@@ -0,0 +1,62 @@
+on: [workflow_dispatch]
+name: cmake-version
+
+jobs:
+  build:
+    continue-on-error: true
+    name: ubuntu:production-dbg
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        cmake_version: [
+          "3.12", "3.13", "3.14", "3.15", "3.16",
+          "3.17", "3.18", "3.19", "3.20", "3.21"
+        ]
+
+    steps:
+    - name: Setup cmake
+      uses: jwlawson/actions-setup-cmake@v1.9
+      with:
+        cmake-version: ${{ matrix.cmake_version }}
+
+    - uses: actions/checkout@v2
+
+    - name: Install dependencies
+      uses: ./.github/actions/install-dependencies
+      with:
+        with-documentation: true
+        with-python-bindings: true
+  
+    - name: Setup caches
+      uses: ./.github/actions/setup-cache
+      with:
+        cache-key: cmake
+  
+    - name: Configure
+      run: |
+        ./configure.sh production --auto-download --static --python-bindings --assertions --tracing --unit-testing --editline --docs \
+          --prefix=$(pwd)/build/install \
+          --werror
+
+    - name: Build
+      run: make -j${{ env.num_proc }}
+      working-directory: build
+
+    - name: ccache Statistics
+      run: ccache -s
+
+    - name: Run tests
+      uses: ./.github/actions/run-tests
+      with:
+        check-examples: true
+        check-python-bindings: true
+        check-unit-tests: true
+
+    - name: Build Documentation
+      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
+