modifies Clauses for Function Contracts
#6062
Workflow file for this run
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
| # Copyright Kani Contributors | |
| # SPDX-License-Identifier: Apache-2.0 OR MIT | |
| name: Kani CI | |
| on: | |
| pull_request: | |
| 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 }} | |
| strategy: | |
| matrix: | |
| os: [macos-12, ubuntu-20.04, ubuntu-22.04] | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ${{ matrix.os }} | |
| - name: Build Kani | |
| run: cargo build-dev | |
| - name: Execute Kani regression | |
| run: ./scripts/kani-regression.sh | |
| write-json-symtab-regression: | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: Build Kani | |
| run: cargo build-dev -- --features write_json_symtab | |
| - name: Run tests | |
| run: | | |
| cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast | |
| cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast | |
| cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast | |
| benchcomp-tests: | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - 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-20.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-20.04 | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: Build Kani using release mode | |
| run: cargo build-dev -- --release | |
| - name: Execute Kani performance tests | |
| run: ./scripts/kani-perf.sh | |
| env: | |
| RUST_TEST_THREADS: 1 | |
| bookrunner: | |
| runs-on: ubuntu-20.04 | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: Build Kani | |
| run: cargo build-dev | |
| - name: Install book runner dependencies | |
| run: ./scripts/setup/install_bookrunner_deps.sh | |
| - name: Generate book runner report | |
| run: cargo run -p bookrunner | |
| env: | |
| DOC_RUST_LANG_ORG_CHANNEL: nightly | |
| - name: Print book runner text results | |
| run: cat build/output/latest/html/bookrunner.txt | |
| - name: Print book runner failures grouped by stage | |
| run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html | |
| - name: Detect unexpected book runner failures | |
| run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt | |
| - 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 |