Merge branch 'main' into no-assume #156
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-11, ubuntu-20.04, ubuntu-22.04] | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v3 | |
| - 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@v3 | |
| - 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@v3 | |
| - 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@v3 | |
| - 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@v3 | |
| - 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 | |
| releasebundle-macos: | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [macos-11] | |
| include: | |
| - os: macos-11 | |
| artifact: kani-latest-x86_64-apple-darwin.tar.gz | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v3 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ${{ matrix.os }} | |
| - name: Build release bundle | |
| run: | | |
| cargo bundle -- latest | |
| cargo package -p kani-verifier | |
| # We can't run macos in a container, so we can only test locally. | |
| # Hopefully any dependency issues won't be unique to macos. | |
| - name: Local install test | |
| if: ${{ matrix.os == 'macos-11' }} | |
| run: | | |
| cargo install --path ./target/package/kani-verifier-*[^e] | |
| cargo-kani setup --use-local-bundle ./${{ matrix.artifact }} | |
| (cd tests/cargo-kani/simple-lib && cargo kani) | |
| (cd tests/cargo-kani/simple-visualize && cargo kani) | |
| (cd tests/cargo-kani/build-rs-works && cargo kani) | |
| - name: Upload artifact | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: ${{ matrix.artifact }} | |
| path: ${{ matrix.artifact }} | |
| if-no-files-found: error | |
| # Aggressively short retention: we don't really need these | |
| retention-days: 3 | |
| releasebundle-ubuntu: | |
| runs-on: ubuntu-20.04 | |
| container: | |
| image: ubuntu:18.04 | |
| volumes: | |
| - /usr/local:/mnt/host-local | |
| steps: | |
| - name: Remove unnecessary software to free up disk space | |
| run: | | |
| # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml | |
| df -h | |
| rm -r /mnt/host-local/lib/android /mnt/host-local/.ghcup | |
| df -h | |
| # This is required before checkout because the container does not | |
| # have Git installed, so cannot run checkout action. The checkout | |
| # action requires Git >=2.18, so use the Git maintainers' PPA. | |
| - name: Install system dependencies | |
| run: | | |
| apt-get update | |
| apt-get install -y software-properties-common apt-utils | |
| add-apt-repository ppa:git-core/ppa | |
| apt-get update | |
| apt-get install -y \ | |
| build-essential bash-completion curl lsb-release sudo g++ gcc flex \ | |
| bison make patch git | |
| curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL \ | |
| https://get.docker.com -o /tmp/install-docker.sh | |
| bash /tmp/install-docker.sh | |
| - name: Checkout Kani | |
| uses: actions/checkout@v3 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-18.04 | |
| - name: Build release bundle | |
| run: | | |
| PATH=/github/home/.cargo/bin:$PATH cargo bundle -- latest | |
| PATH=/github/home/.cargo/bin:$PATH cargo package -p kani-verifier | |
| # -v flag: Use docker socket from host as we're running docker-in-docker | |
| - name: Build container test | |
| run: | | |
| for tag in 20-04 20-04-alt 18-04; do | |
| >&2 echo "Building test container for ${tag}" | |
| docker build -t kani-$tag -f scripts/ci/Dockerfile.bundle-test-ubuntu-$tag . | |
| done | |
| - name: Run installed tests | |
| run: | | |
| for tag in kani-20-04 kani-20-04-alt kani-18-04; do | |
| for dir in simple-lib simple-visualize build-rs-works simple-kissat; do | |
| >&2 echo "Tag $tag: running test $dir" | |
| docker run -v /var/run/docker.sock:/var/run/docker.sock \ | |
| -w /tmp/kani/tests/cargo-kani/$dir $tag cargo kani | |
| done | |
| docker run -v /var/run/docker.sock:/var/run/docker.sock \ | |
| $tag cargo-kani setup \ | |
| --use-local-bundle ./kani-latest-x86_64-unknown-linux-gnu.tar.gz | |
| done | |
| # While the above test OS issues, now try testing with nightly as | |
| # default: | |
| docker run -v /var/run/docker.sock:/var/run/docker.sock \ | |
| -w /tmp/kani/tests/cargo-kani/simple-lib kani-20-04 \ | |
| bash -c "rustup default nightly && cargo kani" | |
| - name: Upload artifact | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: kani-latest-x86_64-unknown-linux-gnu.tar.gz | |
| path: kani-latest-x86_64-unknown-linux-gnu.tar.gz | |
| if-no-files-found: error | |
| # Aggressively short retention: we don't really need these | |
| retention-days: 3 |