[proofs] Fix handling of cycles in LazyProofChain #1777
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| on: [push, pull_request] | |
| name: CI | |
| # Prevents github from relying on clones of homebrew-core or homebrew-cask. | |
| # https://github.com/orgs/Homebrew/discussions/4612 | |
| env: | |
| HOMEBREW_NO_INSTALL_FROM_API: "" | |
| jobs: | |
| build: | |
| strategy: | |
| matrix: | |
| include: | |
| - name: ubuntu:production | |
| os: ubuntu-20.04 | |
| config: production --auto-download --all-bindings --editline --docs | |
| cache-key: production | |
| strip-bin: strip | |
| python-bindings: true | |
| build-documentation: true | |
| check-examples: true | |
| package-name: cvc5-Linux | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump | |
| - name: ubuntu:production-arm64-cross | |
| os: ubuntu-latest | |
| config: production --auto-download --arm64 | |
| cache-key: production-arm64-cross | |
| strip-bin: aarch64-linux-gnu-strip | |
| package-name: cvc5-Linux-arm64 | |
| - name: macos:production | |
| os: macos-13 | |
| config: production --auto-download --all-bindings --editline -DBUILD_GMP=1 | |
| cache-key: production | |
| strip-bin: strip | |
| python-bindings: true | |
| check-examples: true | |
| package-name: cvc5-macOS | |
| macos-target: 10.13 | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump | |
| - name: macos:production-arm64 | |
| os: macos-14 | |
| config: production --auto-download --all-bindings --editline -DBUILD_GMP=1 | |
| cache-key: production-arm64 | |
| strip-bin: strip | |
| python-bindings: true | |
| check-examples: true | |
| package-name: cvc5-macOS-arm64 | |
| macos-target: 11.0 | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump | |
| - name: macos:production-arm64-cross | |
| os: macos-13 | |
| config: production --auto-download --all-bindings --editline --arm64 | |
| cache-key: production-arm64-cross | |
| strip-bin: strip | |
| python-bindings: true | |
| - name: win64:production | |
| os: windows-latest | |
| config: production --auto-download | |
| cache-key: production-win64-native | |
| strip-bin: strip | |
| windows-build: true | |
| shell: 'msys2 {0}' | |
| check-examples: true | |
| exclude_regress: 1-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump | |
| - name: win64:production-cross | |
| os: ubuntu-latest | |
| config: production --auto-download --win64 | |
| cache-key: production-win64-cross | |
| strip-bin: x86_64-w64-mingw32-strip | |
| windows-build: true | |
| package-name: cvc5-Win64 | |
| - name: ubuntu:production-clang | |
| os: ubuntu-20.04 | |
| env: CC=clang CXX=clang++ | |
| config: production --auto-download --no-poly | |
| cache-key: productionclang | |
| check-examples: true | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump | |
| - name: ubuntu:production-dbg | |
| os: ubuntu-20.04 | |
| config: production --auto-download --assertions --tracing --unit-testing --all-bindings --editline --cocoa | |
| cache-key: dbg | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump | |
| python-bindings: true | |
| - name: ubuntu:production-dbg-clang | |
| os: ubuntu-20.04 | |
| env: CC=clang CXX=clang++ | |
| config: production --auto-download --assertions --tracing --cln --gpl | |
| cache-key: dbgclang | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester alf --tester base --tester model --tester synth --tester abduct --tester unsat-core --tester dump | |
| name: ${{ matrix.name }} | |
| runs-on: ${{ matrix.os }} | |
| # cancel already running jobs for the same branch/pr/tag | |
| concurrency: | |
| group: build-${{ github.ref }}-${{ matrix.name }}-${{ github.ref != 'refs/heads/main' || github.run_id }} | |
| cancel-in-progress: ${{ github.repository != 'cvc5/cvc5' || startsWith(github.ref, 'refs/pull/') }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install dependencies | |
| uses: ./.github/actions/install-dependencies | |
| with: | |
| with-documentation: ${{ matrix.build-documentation }} | |
| with-python-bindings: ${{ matrix.python-bindings }} | |
| windows-build: ${{ matrix.windows-build }} | |
| shell: ${{ matrix.shell }} | |
| - name: Setup caches | |
| uses: ./.github/actions/setup-cache | |
| with: | |
| cache-key: ${{ matrix.cache-key }} | |
| shell: ${{ matrix.shell }} | |
| - name: Configure and build | |
| id: configure-and-build | |
| uses: ./.github/actions/configure-and-build | |
| with: | |
| configure-env: ${{ matrix.env }} | |
| configure-config: ${{ matrix.config }} | |
| macos-target: ${{ matrix.macos-target }} | |
| build-shared: ${{ matrix.build-shared }} | |
| build-static: ${{ matrix.build-static }} | |
| strip-bin: ${{ matrix.strip-bin }} | |
| shell: ${{ matrix.shell }} | |
| - name: Run tests | |
| if: matrix.run_regression_args | |
| uses: ./.github/actions/run-tests | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} | |
| check-examples: ${{ matrix.check-examples }} | |
| check-python-bindings: ${{ matrix.python-bindings }} | |
| regressions-args: ${{ matrix.run_regression_args }} | |
| regressions-exclude: ${{ matrix.exclude_regress }} | |
| shell: ${{ matrix.shell }} | |
| - name: Run tests | |
| if: matrix.run_regression_args | |
| uses: ./.github/actions/run-tests | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }} | |
| check-examples: false | |
| check-install: false | |
| check-python-bindings: false | |
| regressions-args: ${{ matrix.run_regression_args }} | |
| regressions-exclude: 1-4 | |
| shell: ${{ matrix.shell }} | |
| - name: Build documentation | |
| if: matrix.build-documentation | |
| uses: ./.github/actions/build-documentation | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} | |
| - name: Create and add shared package to latest and release | |
| if: matrix.package-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) | |
| uses: ./.github/actions/add-package | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} | |
| package-name: ${{ matrix.package-name }}-shared | |
| # when using GITHUB_TOKEN, no further workflows are triggered | |
| github-token-latest: ${{ secrets.GITHUB_TOKEN }} | |
| github-token-release: ${{ secrets.ACTION_USER_TOKEN }} | |
| - name: Create and add static package to latest and release | |
| if: matrix.package-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) | |
| uses: ./.github/actions/add-package | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }} | |
| package-name: ${{ matrix.package-name }}-static | |
| # when using GITHUB_TOKEN, no further workflows are triggered | |
| github-token-latest: ${{ secrets.GITHUB_TOKEN }} | |
| github-token-release: ${{ secrets.ACTION_USER_TOKEN }} | |
| update-pr: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'cvc5/cvc5' && github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| concurrency: | |
| group: update-pr | |
| steps: | |
| - name: Automatically update PR | |
| uses: adRise/[email protected] | |
| with: | |
| token: ${{ secrets.ACTION_USER_TOKEN }} | |
| base: 'main' | |
| sort: 'created' | |
| direction: 'asc' | |
| required_approval_count: 1 |