Update charon patch #665
Workflow file for this run
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
| # Copyright Kani Contributors | |
| # SPDX-License-Identifier: Apache-2.0 OR MIT | |
| name: Kani CI | |
| on: | |
| pull_request: | |
| merge_group: | |
| push: | |
| # Not just any push, as that includes tags. | |
| # We don't want to re-trigger this workflow when tagging an existing commit. | |
| branches: | |
| - '**' | |
| env: | |
| RUST_BACKTRACE: 1 | |
| jobs: | |
| regression: | |
| runs-on: ${{ matrix.os }} | |
| permissions: | |
| contents: read | |
| strategy: | |
| matrix: | |
| os: [macos-13, ubuntu-22.04, ubuntu-24.04, macos-14, ubuntu-24.04-arm] | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v5 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ${{ matrix.os }} | |
| - name: Execute Kani regression | |
| run: ./scripts/kani-regression.sh | |
| benchcomp-tests: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v5 | |
| - name: Install benchcomp dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y python3-pip | |
| pushd tools/benchcomp && pip3 install -r requirements.txt | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-24.04 | |
| - name: Build Kani using release mode | |
| run: cargo build-dev -- --release | |
| - name: Run benchcomp unit and regression tests | |
| run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run | |
| perf: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v5 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-24.04 | |
| - name: Execute Kani performance tests | |
| run: ./scripts/kani-perf.sh | |
| env: | |
| RUST_TEST_THREADS: 1 | |
| llbc-regression: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: read | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v5 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-24.04 | |
| # Patch Charon so that it compiles. This is temporary until we're able to | |
| # upgrade the pinned commit which requires fixing | |
| # https://github.com/AeneasVerif/charon/issues/806 and updating the | |
| # mir-to-ullbc code | |
| - name: Patch Charon | |
| run: cd charon && git apply ../scripts/charon-patch.diff | |
| - name: Build Kani with Charon | |
| run: cargo build-dev -- --features cprover --features llbc | |
| - name: Run tests | |
| run: ./scripts/kani-llbc-regression.sh | |
| documentation: | |
| runs-on: ubuntu-24.04 | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v5 | |
| with: | |
| submodules: recursive | |
| - name: Install book dependencies | |
| run: ./scripts/setup/ubuntu/install_doc_deps.sh | |
| # On one OS only, build the documentation, too. | |
| - name: Build Documentation | |
| run: ./scripts/build-docs.sh | |
| # When we're pushed to main branch, only then actually publish the docs. | |
| - name: Publish Documentation | |
| if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }} | |
| uses: JamesIves/github-pages-deploy-action@v4 | |
| with: | |
| branch: gh-pages | |
| folder: docs/book/ | |
| single-commit: true |