Add CI test for --use-local-toolchain #3
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 | ||
| # | ||
| # Job to check if the setup flow and associated flags are working as expected | ||
| # | ||
| # This will run everytime there's a change to main | ||
| name: Check Setup | ||
| on: | ||
| pull_request: | ||
| push: | ||
| branches: | ||
| - 'main' | ||
| jobs: | ||
| build_bundle_macos: | ||
| name: BuildBundle-MacOs | ||
| runs-on: macos-13 | ||
| permissions: | ||
| contents: write | ||
| outputs: | ||
| version: ${{ steps.bundle.outputs.version }} | ||
| bundle: ${{ steps.bundle.outputs.bundle }} | ||
| package: ${{ steps.bundle.outputs.package }} | ||
| crate_version: ${{ steps.bundle.outputs.crate_version }} | ||
| steps: | ||
| - name: Checkout code | ||
| uses: actions/checkout@v4 | ||
| - name: Setup Kani Dependencies | ||
| uses: ./.github/actions/setup | ||
| with: | ||
| os: macos-13 | ||
| - name: Build bundle | ||
| id: bundle | ||
| uses: ./.github/actions/build-bundle | ||
| with: | ||
| os: macos-13 | ||
| arch: x86_64-apple-darwin | ||
| build_bundle_linux: | ||
| name: BuildBundle-Linux | ||
| runs-on: ubuntu-20.04 | ||
| outputs: | ||
| # The bundle version (latest or the version to be released) | ||
| version: ${{ steps.bundle.outputs.version }} | ||
| bundle: ${{ steps.bundle.outputs.bundle }} | ||
| package: ${{ steps.bundle.outputs.package }} | ||
| crate_version: ${{ steps.bundle.outputs.crate_version }} | ||
| container: | ||
| # Build using ubuntu 18 due to compatibility issues with older OS. | ||
| image: ubuntu:18.04 | ||
| volumes: | ||
| - /usr/local:/mnt/host-local | ||
| steps: | ||
| - name: Free up docker 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 and python 3.7, so use the Git maintainers' PPA. | ||
| # and the "deadsnakes" PPA, as the default version of python on ubuntu 22.04 is Python 3.10 | ||
| - name: Install system dependencies | ||
| run: | | ||
| apt-get update | ||
| apt-get install -y software-properties-common apt-utils | ||
| add-apt-repository ppa:git-core/ppa | ||
| add-apt-repository ppa:deadsnakes/ppa | ||
| apt-get update | ||
| apt-get install -y \ | ||
| build-essential bash-completion curl lsb-release sudo g++ gcc flex \ | ||
| bison make patch git python3.7 python3.7-dev python3.7-distutils | ||
| update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1 | ||
| curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py | ||
| python3 get-pip.py --force-reinstall | ||
| rm get-pip.py | ||
| - name: Checkout Kani | ||
| uses: actions/checkout@v3 | ||
| - name: Setup Kani Dependencies | ||
| uses: ./.github/actions/setup | ||
| with: | ||
| os: ubuntu-18.04 | ||
| - name: Build bundle | ||
| id: bundle | ||
| uses: ./.github/actions/build-bundle | ||
| with: | ||
| os: linux | ||
| arch: x86_64-unknown-linux-gnu | ||
| test-use-local-toolchain: | ||
| name: TestLocalToolchain | ||
| strategy: | ||
| matrix: | ||
| os: [macos-13, ubuntu-20.04, ubuntu-22.04] | ||
| include: | ||
| - os: macos-13 | ||
| rust_target: x86_64-apple-darwin | ||
| prev_job: ${{ needs.build_bundle_macos.outputs }} | ||
| - os: ubuntu-20.04 | ||
| rust_target: x86_64-unknown-linux-gnu | ||
| - prev_job: ${{ needs.build_bundle_linux.outputs }} | ||
| - os: ubuntu-22.04 | ||
| rust_target: x86_64-unknown-linux-gnu | ||
| - prev_job: ${{ needs.build_bundle_linux.outputs }} | ||
| runs-on: ${{ matrix.os }} | ||
| steps: | ||
| - name: Download bundle | ||
| uses: actions/download-artifact@v3 | ||
| with: | ||
| name: ${{ matrix.prev_job.bundle }} | ||
| - name: Download kani-verifier crate | ||
| uses: actions/download-artifact@v3 | ||
| with: | ||
| name: ${{ matrix.prev_job.package }} | ||
| - name: Check download | ||
| run: | | ||
| ls -lh . | ||
| - name: Get toolchain version used to setup kani | ||
| run: | | ||
| tar zxvf ${{ matrix.prev_job.bundle }} | ||
| DATE=$(cat kani-${{ matrix.prev_job.crate_version }}/rust_toolchain_version | cut -d'-' -f2,3,4) | ||
| echo "Nightly date: $DATE" | ||
| echo "DATE=$DATE" >> $GITHUB_ENV | ||
| # - name: Extract nightly version date from the release bundle | ||
| # id: extract-date | ||
| # run: | | ||
| # tar zxvf ${{ matrix.prev_job.package }} | ||
| # DATE=$(grep 'channel' | cut -d '=' -f2 | tr -d ' "' | cut -d'-' -f2-) | ||
| # echo "Nightly date: $DATE" | ||
| # echo "DATE=$DATE" >> $GITHUB_ENV | ||
| # - name: Create a custom toolchain directory | ||
| # run: mkdir -p ${{ github.workspace }}/custom_toolchain | ||
| # - name: Fetch the nightly tarball | ||
| # run: | | ||
| # echo "Downloading Rust toolchain from rust server." | ||
| # curl --proto '=https' --tlsv1.2 -O https://static.rust-lang.org/dist/$DATE/rust-nightly-${{ matrix.rust_target }}.tar.gz | ||
| # tar -xzf rust-nightly-${{ matrix.rust_target }}.tar.gz | ||
| # ./rust-nightly-${{ matrix.rust_target }}/install.sh --prefix=${{ github.workspace }}/custom_toolchain | ||
| # - name: Ensure installation is correct | ||
| # run: | | ||
| # cargo kani setup --use-local-toolchain ${{ github.workspace }}/custom_toolchain/ | ||
| # - name: Ensure that the rustup toolchain is not present | ||
| # run: | | ||
| # if [ ! -e "~/.rustup/toolchains/" ]; then | ||
| # echo "Default toolchain file does not exist. Proceeding with running tests." | ||
| # else | ||
| # echo "::error::Default toolchain exists despite not installing." | ||
| # exit 1 | ||
| # fi | ||
| # - name: Run cargo-kani tests | ||
| # run: | | ||
| # for dir in function multiple-harnesses verbose; do | ||
| # >&2 echo "Running test $dir" | ||
| # pushd ./tests/cargo-ui/$dir | ||
| # cargo kani | ||
| # popd | ||
| # done | ||
| # - name: Check --help and --version | ||
| # run: | | ||
| # cargo kani --help && cargo kani --version | ||
| # - name: Run standalone kani test | ||
| # run: | | ||
| # >&2 echo "Running test on file $dir" | ||
| # pushd ./tests/kani/$dir | ||
| # kani bool_ref.rs | ||
| # popd | ||
