From c648f18af916af5975b9a85350a1c860c8665197 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 12 Aug 2026 11:19:21 -0500 Subject: [PATCH] Cache the cvc5 artifacts required to test the Pythonic API Building cvc5 from scratch on every CI run is wasteful when its code has not changed. Cache the artifacts the tests actually need, keyed on the cvc5 commit, and skip the build when they can be restored. The cached artifacts are the Python bindings package and the cvc5 shared libraries it links against. The bindings embed an absolute rpath into the build tree, which is stable across runs, so they can be restored and used in place. Skipping the build additionally requires a hit on the dependencies cache: in a shared build, which --python-bindings requires, some dependencies, libpoly among them, are built as shared libraries under deps/install/lib and are loaded at run time. Installing the build dependencies is skipped along with the build. All that action provides is needed to build cvc5: the compilers and headers, ccache, and the num_proc variable. The libraries the cached artifacts load at run time are either part of the runner image, libgmp10 and libstdc++, or come from the cached build/deps. Note that this relies on the bindings not being linked against CLN, whose runtime package is not part of the runner image: --gpl only permits GPL dependencies, it does not select the CLN implementation, which is what --cln does. The cache keys track the configuration cvc5 is built with, now defined once in the CVC5_CONFIG variable, rather than the workflow file, so that unrelated changes to the workflow do not discard the cached artifacts. Finally, actually use ccache. The workflow set up a ccache cache and configured it, but cvc5 only uses ccache if the compiler launchers are passed to CMake, which its own CI does but this workflow did not, so nothing was ever cached. This matters because the artifacts cache turns over whenever the cvc5 default branch advances; a working ccache makes those rebuilds incremental. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 90 +++++++++++++++++++++++++++++++++++----- 1 file changed, 79 insertions(+), 11 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 616e04c..6775f98 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -5,6 +5,12 @@ jobs: build: runs-on: ubuntu-latest + env: + # The configuration cvc5 is built with. The cache keys below track this + # value instead of the workflow file, so that unrelated changes to the + # workflow do not invalidate the cached artifacts. + CVC5_CONFIG: production --auto-download --python-bindings --cocoa --gpl + # cancel already running jobs for the same branch/pr/tag concurrency: group: build-${{ github.ref }} @@ -12,7 +18,7 @@ jobs: steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v7 - uses: psf/black@stable with: @@ -20,24 +26,76 @@ jobs: src: "cvc5_pythonic_api" version: "24.10.0" - - uses: actions/checkout@v2 + - uses: actions/checkout@v7 with: repository: cvc5/cvc5 path: cvc5 - + + - name: Identify cvc5 build inputs + id: cvc5-info + shell: bash + run: | + echo "sha=$(git -C cvc5 rev-parse HEAD)" >> "$GITHUB_OUTPUT" + echo "python=$(python3 -c 'import sys; print("%d.%d" % sys.version_info[:2])')" >> "$GITHUB_OUTPUT" + echo "config=$(printf '%s' "$CVC5_CONFIG" | sha256sum | cut -c1-16)" >> "$GITHUB_OUTPUT" + + # The artifacts needed to run the tests: the Python bindings package and + # the cvc5 shared libraries it is linked against. The bindings embed an + # absolute rpath to ${{ github.workspace }}/cvc5/build/src{,/parser}, which + # is stable across runs, so they can be restored and used as-is. + - name: Setup cvc5 artifacts cache + id: cvc5-cache + uses: actions/cache@v6 + with: + path: | + cvc5/build/src/api/python/cvc5 + cvc5/build/src/*.so* + cvc5/build/src/parser/*.so* + key: cvc5-pythonic-api-artifacts-${{ runner.os }}-py${{ steps.cvc5-info.outputs.python }}-${{ steps.cvc5-info.outputs.sha }}-${{ steps.cvc5-info.outputs.config }} + + # In a shared build (required by --python-bindings) some dependencies, e.g. + # libpoly, are built as shared libraries under deps/install/lib that cvc5 + # loads at run time, so this cache is needed for testing too, not just for + # building. + - name: Setup dependencies cache + id: deps-cache + uses: actions/cache@v6 + with: + path: cvc5/build/deps + key: cvc5-pythonic-api-deps-${{ hashFiles('cvc5/cmake/**') }}-${{ steps.cvc5-info.outputs.config }} + + - name: Check whether cvc5 has to be built + id: build-cvc5 + shell: bash + run: | + if [ "${{ steps.cvc5-cache.outputs.cache-hit }}" = "true" ] && + [ "${{ steps.deps-cache.outputs.cache-hit }}" = "true" ]; then + echo "Reusing the cached cvc5 artifacts for ${{ steps.cvc5-info.outputs.sha }}" + echo "needed=false" >> "$GITHUB_OUTPUT" + else + echo "needed=true" >> "$GITHUB_OUTPUT" + fi + + # Everything this installs is only needed to build cvc5: the compilers and + # headers, ccache, and the num_proc variable. The libraries that the cached + # artifacts load at run time are either part of the runner image (libgmp10, + # libstdc++) or come from the cached cvc5/build/deps. - name: Install dependencies + if: steps.build-cvc5.outputs.needed == 'true' uses: ./cvc5/.github/actions/install-dependencies with: with-documentation: false - name: Setup ccache cache - uses: actions/cache@v4 + if: steps.build-cvc5.outputs.needed == 'true' + uses: actions/cache@v6 with: path: ccache-dir key: cvc5-pythonic-api-ccache-${{ github.sha }} restore-keys: cvc5-pythonic-api-ccache- - name: Configure ccache + if: steps.build-cvc5.outputs.needed == 'true' shell: bash run: | ccache --set-config=cache_dir=${{ github.workspace }}/ccache-dir @@ -46,19 +104,29 @@ jobs: ccache -M 500M ccache -z - - name: Setup dependencies cache - uses: actions/cache@v4 - with: - path: cvc5/build/deps - key: cvc5-pythonic-api-deps-${{ hashFiles('cvc5/cmake/**') }}-${{ hashFiles('.github/**') }} - - name: Build cvc5 + if: steps.build-cvc5.outputs.needed == 'true' run: | cd cvc5/ - ./configure.sh production --auto-download --python-bindings --cocoa --gpl + # $CVC5_CONFIG is unquoted on purpose: the flags must be split into + # separate arguments. cvc5 only uses ccache when it is told to, so the + # compiler launchers have to be passed explicitly, as its own CI does. + ./configure.sh $CVC5_CONFIG \ + -DCMAKE_C_COMPILER_LAUNCHER=ccache -DCMAKE_CXX_COMPILER_LAUNCHER=ccache cd build/ + ccache --set-config="base_dir=$(pwd)" make -j${{ env.num_proc }} + - name: Report the ccache statistics + if: steps.build-cvc5.outputs.needed == 'true' + run: ccache -s + + - name: Check the cached cvc5 artifacts + if: steps.build-cvc5.outputs.needed != 'true' + run: python3 -c 'import cvc5; print(cvc5.__file__)' + env: + PYTHONPATH: cvc5/build/src/api/python + - name: Test cvc5 pythonic API run: | make test