From 0ddbf090c7f7f33ce724df456daecf84d807e793 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 11 Oct 2021 09:31:21 -0700 Subject: [PATCH] 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. --- .../actions/build-documentation/action.yml | 19 ++ .../actions/install-dependencies/action.yml | 78 +++++++ .github/actions/run-tests/action.yml | 54 +++++ .github/actions/setup-cache/action.yml | 69 +++++++ .github/workflows/ci.yml | 193 ++---------------- .github/workflows/cmake-version.yml | 62 ++++++ CMakeLists.txt | 3 - docs/api/java/CMakeLists.txt | 2 +- 8 files changed, 298 insertions(+), 182 deletions(-) create mode 100644 .github/actions/build-documentation/action.yml create mode 100644 .github/actions/install-dependencies/action.yml create mode 100644 .github/actions/run-tests/action.yml create mode 100644 .github/actions/setup-cache/action.yml create mode 100644 .github/workflows/cmake-version.yml 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 \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 \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 + diff --git a/CMakeLists.txt b/CMakeLists.txt index 2a72cf2c3..3d173c845 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -247,9 +247,6 @@ endif() #-----------------------------------------------------------------------------# # Shared/static libraries -# -# This needs to be set before any find_package(...) command since we want to -# search for static libraries with suffix .a. # Embed the installation prefix as an RPATH in the executable such that the # linker can find our libraries (such as libcvc5parser) when executing the diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 96a5d80b6..20a5d91a3 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -29,7 +29,7 @@ if(BUILD_BINDINGS_JAVA) OUTPUT "${JAVADOC_INDEX_FILE}" COMMAND ${Java_JAVADOC_EXECUTABLE} cvc5 - --source-path ${CMAKE_SOURCE_DIR}/src/api/java/ + -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar -notimestamp -- 2.30.2