Merge remote-tracking branch 'upstream/main' into leibnizRe #42
This file contains hidden or 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: | |
| setup-release-pages: | |
| name: Set up release pages | |
| runs-on: ubuntu-latest | |
| concurrency: | |
| group: setup-release-pages | |
| cancel-in-progress: false | |
| steps: | |
| - name: Checkout code | |
| if: (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) | |
| uses: actions/checkout@v4 | |
| - name: Set up latest page | |
| if: github.ref == 'refs/heads/main' | |
| uses: ./.github/actions/setup-latest | |
| - name: Set up new version page | |
| if: startsWith(github.ref, 'refs/tags/') | |
| uses: ./.github/actions/setup-new-version | |
| with: | |
| # When using GITHUB_TOKEN, no further workflows are triggered | |
| # See https://github.com/cvc5/cvc5/pull/8512 | |
| github-token-release: ${{ secrets.ACTION_USER_TOKEN }} | |
| builds: | |
| needs: [setup-release-pages] | |
| strategy: | |
| matrix: | |
| has-tag: | |
| - ${{ startsWith(github.ref, 'refs/tags/') }} | |
| build: | |
| - name: ubuntu:production | |
| os: ubuntu-22.04 | |
| 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-Linux-x86_64 | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump | |
| - name: ubuntu:safe-mode | |
| os: ubuntu-22.04 | |
| config: safe-mode --auto-download --all-bindings --editline -DBUILD_GMP=1 | |
| cache-key: production-safe | |
| strip-bin: strip | |
| python-bindings: true | |
| java-bindings: true | |
| check-examples: true | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester proof --tester cpc --tester model --tester synth --tester abduct --tester dump | |
| - name: ubuntu:stable-mode | |
| os: ubuntu-22.04 | |
| config: stable-mode --auto-download --all-bindings --editline -DBUILD_GMP=1 | |
| cache-key: production-stable | |
| strip-bin: strip | |
| python-bindings: true | |
| java-bindings: true | |
| check-examples: true | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester proof --tester cpc --tester model --tester dump | |
| - name: ubuntu:production-arm64 | |
| os: ubuntu-22.04-arm | |
| 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-Linux-arm64 | |
| 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 | |
| - 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 | |
| java-version: 11 | |
| 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-arm64 | |
| os: windows-11-arm | |
| config: production --auto-download --all-bindings | |
| cache-key: production-win64-native-arm64 | |
| strip-bin: strip | |
| python-bindings: true | |
| java-bindings: true | |
| java-version: 21 | |
| windows-build: true | |
| shell: 'msys2 {0}' | |
| check-examples: true | |
| package-name: cvc5-Win64-arm64 | |
| 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-22.04 | |
| config: production --static --static-binary --auto-download --wasm-web=no-modular-static-page | |
| cache-key: productionwasm | |
| wasm-build: true | |
| wasm-pkg-name: cvc5-Wasm | |
| build-shared: false | |
| build-static: true | |
| - name: ubuntu:production-clang | |
| os: ubuntu-22.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 | |
| # Job used to build the documentation | |
| - name: ubuntu:production-dbg | |
| os: ubuntu-24.04 # Use Doxygen version from this Ubuntu release | |
| config: >- | |
| production --auto-download --assertions --tracing --unit-testing --editline | |
| --cocoa --gpl --all-bindings --docs --docs-ga -DBUILD_GMP=1 | |
| cache-key: dbg | |
| python-bindings: true | |
| java-version: 21 # Use Javadoc from this Java version | |
| build-documentation: true | |
| exclude_regress: 3-4 | |
| run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump | |
| - name: ubuntu:production-dbg-clang | |
| os: ubuntu-22.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-22.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: ubuntu:production-arm64-gpl | |
| os: ubuntu-22.04-arm | |
| 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-Linux-arm64 | |
| 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 | |
| java-version: 11 | |
| macos-target: 11.0 | |
| gpl-tag: -gpl | |
| exclude: | |
| - has-tag: false | |
| build: | |
| name: ubuntu:production-gpl | |
| - has-tag: false | |
| build: | |
| name: ubuntu:production-arm64-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 | |
| # Ensure that the Java bindings, Java API tests, and Java examples are compatible | |
| # with the minimum required Java version (currently Java 8). | |
| - uses: actions/setup-java@v4 | |
| with: | |
| distribution: 'temurin' | |
| java-version: ${{ matrix.build.java-version || '8' }} | |
| - name: Setup CMake | |
| uses: ./.github/actions/setup-cmake | |
| # Exclude Linux ARM64 runners, which are currently unsupported | |
| if: runner.os == 'Linux' && ! contains(runner.arch, 'ARM') | |
| with: | |
| shell: ${{ matrix.build.shell }} | |
| - 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 }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Create and add static package to latest and release | |
| id: create-static-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.static-build-dir }} | |
| package-name: ${{ matrix.build.package-name }}-static${{ matrix.build.gpl-tag }} | |
| shell: ${{ matrix.build.shell }} | |
| - name: Create and add WASM to latest and release | |
| if: matrix.build.wasm-pkg-name && (github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/tags/')) | |
| uses: ./.github/actions/add-wasm | |
| with: | |
| build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }} | |
| wasm-name: ${{ matrix.build.wasm-pkg-name }}${{ matrix.build.gpl-tag }} | |
| 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-static-package.outputs.install-path }} | |
| jar-libs-dir: cvc5-libs | |
| jar-name: ${{ matrix.build.package-name }}${{ matrix.build.gpl-tag }}-java-api | |
| shell: ${{ matrix.build.shell }} | |
| cleanup-artifacts: | |
| name: Clean up artifacts from latest | |
| if: github.ref == 'refs/heads/main' | |
| runs-on: ubuntu-latest | |
| needs: [builds] | |
| concurrency: | |
| group: cleanup-artifacts | |
| cancel-in-progress: false | |
| steps: | |
| - name: Prune old assets | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| shell: 'python3 {0}' | |
| run: | | |
| import subprocess | |
| import json | |
| from datetime import datetime, timezone, timedelta | |
| import re | |
| import os | |
| repo = os.environ["GITHUB_REPOSITORY"] | |
| # Fetch latest release info | |
| release_json = subprocess.run( | |
| ["gh", "api", f"repos/{repo}/releases/tags/latest"], | |
| capture_output=True, | |
| text=True, | |
| check=True | |
| ).stdout | |
| release = json.loads(release_json) | |
| assets = release.get("assets", []) | |
| now = datetime.now(timezone.utc) | |
| seven_days_ago = now - timedelta(days=7) | |
| # Set of assets to delete | |
| delete_ids = set() | |
| # Dictionary to group assets by prefix and date | |
| # for filenames like "prefix-date-sha.ext" | |
| # Structure: { prefix: { date: [asset1, asset2, ...] } } | |
| prefix_date_assets = {} | |
| # Group assets by prefix and date (excluding assets older than 7 days) | |
| for asset in assets: | |
| name = asset["name"] | |
| created_at = datetime.fromisoformat(asset["created_at"].replace("Z", "+00:00")) | |
| # Mark for deletion assets older than 7 days | |
| if created_at < seven_days_ago: | |
| delete_ids.add((asset["id"], asset["name"])) | |
| continue | |
| # Extract prefix and date from filenames like: | |
| # "prefix-YYYY-MM-DD-sha.ext" | |
| m = re.match(r"^(.+)-(\d{4}-\d{2}-\d{2})-.*$", name) | |
| if not m: | |
| continue | |
| prefix, date_str = m.group(1), m.group(2) | |
| # Append asset to the relevant prefix/date group | |
| prefix_date_assets.setdefault(prefix, {}).setdefault(date_str, []).append(asset) | |
| keep_ids = set() | |
| # For each prefix, keep only: | |
| # - The 2 most recent dates | |
| # - The newest asset for each date | |
| for prefix, date_assets in prefix_date_assets.items(): | |
| sorted_dates = sorted(date_assets.keys(), reverse=True) | |
| top_two_dates = sorted_dates[:2] | |
| for date in top_two_dates: | |
| newest_asset = max(date_assets[date], key=lambda a: a["created_at"]) | |
| keep_ids.add(newest_asset["id"]) | |
| # Mark for deletion all assets not in keep_ids | |
| for asset in assets: | |
| if asset["id"] not in keep_ids: | |
| delete_ids.add((asset["id"], asset["name"])) | |
| # Delete old assets | |
| for asset_id, asset_name in delete_ids: | |
| print(f"Deleting asset {asset_name} ({asset_id})") | |
| subprocess.run([ | |
| "gh", "api", | |
| "--method", "DELETE", | |
| f"repos/{repo}/releases/assets/{asset_id}" | |
| ], check=True) |