Doc #30183
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: | |
| builds: | |
| strategy: | |
| matrix: | |
| has-tag: | |
| - ${{ startsWith(github.ref, 'refs/tags/') }} | |
| build: | |
| - name: ubuntu:production | |
| os: ubuntu-20.04 | |
| config: production --auto-download --all-bindings --editline --docs --docs-ga -DBUILD_GMP=1 | |
| cache-key: production | |
| strip-bin: strip | |
| python-bindings: true | |
| java-bindings: true | |
| build-documentation: true | |
| check-examples: true | |
| package-name: cvc5-Linux-x86_64 | |
| 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 | |
| java-bindings: true | |
| check-examples: true | |
| package-name: cvc5-macOS-x86_64 | |
| 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 | |
| java-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 --all-bindings | |
| cache-key: production-win64-native | |
| strip-bin: strip | |
| python-bindings: true | |
| java-bindings: true | |
| windows-build: true | |
| shell: 'msys2 {0}' | |
| check-examples: true | |
| package-name: cvc5-Win64-x86_64 | |
| 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 | |
| - name: wasm:production | |
| os: ubuntu-20.04 | |
| config: production --static --static-binary --auto-download --wasm=JS --wasm-flags='-s MODULARIZE' | |
| cache-key: productionwasm | |
| wasm-build: true | |
| build-shared: false | |
| build-static: true | |
| - 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 --gpl | |
| 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 cpc --tester alethe --tester base --tester model --tester synth --tester abduct --tester unsat-core --tester dump | |
| # GPL versions | |
| - name: ubuntu:production-gpl | |
| os: ubuntu-20.04 | |
| config: production --auto-download --editline --gpl --cln --glpk --cocoa -DBUILD_GMP=1 -DBUILD_CLN=1 | |
| cache-key: production-gpl | |
| strip-bin: strip | |
| package-name: cvc5-Linux-x86_64 | |
| gpl-tag: -gpl | |
| - name: macos:production-gpl | |
| os: macos-13 | |
| config: production --auto-download --editline --gpl --cln --glpk --cocoa -DBUILD_GMP=1 -DBUILD_CLN=1 | |
| cache-key: production-gpl | |
| strip-bin: strip | |
| package-name: cvc5-macOS-x86_64 | |
| macos-target: 10.13 | |
| gpl-tag: -gpl | |
| - name: macos:production-arm64-gpl | |
| os: macos-14 | |
| config: production --auto-download --editline --gpl --cln --glpk --cocoa -DBUILD_GMP=1 -DBUILD_CLN=1 | |
| cache-key: production-arm64-gpl | |
| strip-bin: strip | |
| package-name: cvc5-macOS-arm64 | |
| macos-target: 11.0 | |
| gpl-tag: -gpl | |
| exclude: | |
| - has-tag: false | |
| build: | |
| name: ubuntu:production-gpl | |
| - has-tag: false | |
| build: | |
| name: macos:production-gpl | |
| - has-tag: false | |
| build: | |
| name: macos:production-arm64-gpl | |
| name: ${{ matrix.build.name }} | |
| runs-on: ${{ matrix.build.os }} | |
| # cancel already running jobs for the same branch/pr/tag | |
| concurrency: | |
| group: build-${{ github.ref }}-${{ matrix.build.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.build-documentation }} | |
| windows-build: ${{ matrix.build.windows-build }} | |
| wasm-build: ${{ matrix.build.wasm-build }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Setup caches | |
| uses: ./.github/actions/setup-cache | |
| with: | |
| cache-key: ${{ matrix.build.cache-key }} | |
| install-ethos: ${{ contains(matrix.build.run_regression_args, '--tester cpc') }} | |
| install-carcara: ${{ contains(matrix.build.run_regression_args, '--tester alethe') }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Configure and build | |
| id: configure-and-build | |
| uses: ./.github/actions/configure-and-build | |
| with: | |
| configure-env: ${{ matrix.build.env }} | |
| configure-config: ${{ matrix.build.config }} | |
| macos-target: ${{ matrix.build.macos-target }} | |
| build-shared: ${{ matrix.build.build-shared }} | |
| build-static: ${{ matrix.build.build-static }} | |
| strip-bin: ${{ matrix.build.strip-bin }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Run tests | |
| if: matrix.build.run_regression_args | |
| uses: ./.github/actions/run-tests | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.shared-build-dir }} | |
| check-examples: ${{ matrix.build.check-examples }} | |
| check-python-bindings: ${{ matrix.build.python-bindings }} | |
| regressions-args: ${{ matrix.build.run_regression_args }} | |
| regressions-exclude: ${{ matrix.build.exclude_regress }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Run tests | |
| if: matrix.build.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.build.run_regression_args }} | |
| regressions-exclude: 1-4 | |
| shell: ${{ matrix.build.shell }} | |
| - name: Build documentation | |
| if: matrix.build.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 | |
| id: create-shared-package | |
| if: matrix.build.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.build.package-name }}-shared${{ matrix.build.gpl-tag }} | |
| # when using GITHUB_TOKEN, no further workflows are triggered | |
| github-token-latest: ${{ secrets.GITHUB_TOKEN }} | |
| github-token-release: ${{ secrets.ACTION_USER_TOKEN }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Create and add static package to latest and release | |
| if: matrix.build.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.build.package-name }}-static${{ matrix.build.gpl-tag }} | |
| # when using GITHUB_TOKEN, no further workflows are triggered | |
| github-token-latest: ${{ secrets.GITHUB_TOKEN }} | |
| github-token-release: ${{ secrets.ACTION_USER_TOKEN }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Create and add JAR to latest and release | |
| if: matrix.build.java-bindings && matrix.build.package-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) | |
| uses: ./.github/actions/add-jar | |
| with: | |
| install-path: ${{ steps.create-shared-package.outputs.install-path }} | |
| jar-libs-dir: cvc5-libs | |
| jar-name: ${{ matrix.build.package-name }}${{ matrix.build.gpl-tag }}-java-api | |
| github-token-latest: ${{ secrets.GITHUB_TOKEN }} | |
| github-token-release: ${{ secrets.ACTION_USER_TOKEN }} | |
| shell: ${{ matrix.build.shell }} |