support async functions #9326
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
| name: ci | |
| on: | |
| push: | |
| branches: | |
| - "main" | |
| workflow_dispatch: | |
| pull_request: | |
| types: [opened, synchronize, reopened] | |
| # Cancel a workflow iff the branch for the pull request got updated | |
| # | |
| # How: | |
| # - This creates a concurrency group for workflow runs; | |
| # - When the workflow runs, it cancels in-progress runs if the concurrency group is the same | |
| # - The group names are ci-<pr number> (in the case of PRs) and ci-<SHA> for main | |
| # - This means that we still run CI for every commit on main (but those runs don't get updated anyway) | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.event.push.after }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: write | |
| jobs: | |
| # check if formatting is correct | |
| fmt: | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| - name: setup verusfmt | |
| run: curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/latest/download/verusfmt-installer.sh | sh | |
| - name: check rustfmt/verusfmt | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo fmt -- --check | |
| - name: check cargo fmt for vargo | |
| working-directory: ./tools/vargo | |
| run: cargo fmt -- --check | |
| # run linter (clippy) | |
| clippy: | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| components: clippy | |
| - name: clippy check codebase | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clippy -- -D warnings | |
| - name: clippy check vargo | |
| working-directory: ./tools/vargo | |
| run: cargo clippy -- -D warnings | |
| # check if it builds and runs on macos, running the full test suite | |
| # (in release mode because it makes a huge difference) | |
| full-test: | |
| runs-on: macos-14 | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: get z3 | |
| working-directory: ./source | |
| run: | | |
| ./tools/get-z3.sh | |
| echo z3 version `./z3 --version` | |
| - name: get cvc5 | |
| working-directory: ./source | |
| run: | | |
| ./tools/get-cvc5.sh | |
| echo cvc5 version `./cvc5 --version` | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| - name: setup nextest | |
| uses: taiki-e/install-action@nextest | |
| - name: build | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| RUSTFLAGS="-C debug-assertions" vargo build --release | |
| - name: full tests | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| RUSTFLAGS="-C debug-assertions" VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run --release -p air | |
| RUSTFLAGS="-C debug-assertions" VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run --release -p rust_verify_test | |
| # check cvc5 | |
| vargo run --release -p rust_verify -- -V cvc5 ../examples/assorted_demo.rs | |
| - name: build line-count tool | |
| working-directory: ./source/tools/line_count | |
| run: cargo build | |
| # check if it builds and that basic tests pass on our main supported platforms | |
| basic-test: | |
| strategy: | |
| matrix: | |
| build: [macos-x86_64, linux, windows] | |
| include: | |
| - build: macos-x86_64 | |
| os: macos-15-intel | |
| - build: linux | |
| os: ubuntu-22.04 | |
| - build: windows | |
| os: windows-2022 | |
| runs-on: ${{ matrix.os }} | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: get z3 | |
| working-directory: ./source | |
| run: | | |
| ./tools/get-z3.sh | |
| echo z3 version `./z3 --version` | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| - name: setup nextest | |
| uses: taiki-e/install-action@nextest | |
| - name: build | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build | |
| - name: basic tests | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run -p rust_verify_test --test basic | |
| - name: build line-count tool | |
| working-directory: ./source/tools/line_count | |
| run: cargo build | |
| # check if esoteric conficurations build | |
| smoke-test: | |
| strategy: | |
| matrix: | |
| features: [record-history, no-std, no-alloc, singular] | |
| runs-on: macos-14 | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: get z3 | |
| working-directory: ./source | |
| run: | | |
| ./tools/get-z3.sh | |
| echo z3 version `./z3 --version` | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| - name: setup nextest | |
| uses: taiki-e/install-action@nextest | |
| - name: download singular | |
| if: matrix.features == 'singular' | |
| run: curl -fLO https://github.com/verus-lang/verus/releases/download/dependency/singular-4.3.2/Singular-4-3-2_M1.dmg | |
| - name: build | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| case "${{ matrix.features }}" in | |
| "singular") | |
| hdiutil attach ../Singular-4-3-2_M1.dmg | |
| DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/Volumes/Singular4.3.2/Singular.app/Contents/lib VERUS_SINGULAR_PATH=/Volumes/Singular4.3.2/Singular.app/Contents/bin/Singular VERUS_Z3_PATH="$(pwd)/z3" vargo build --features singular | |
| ;; | |
| "record-history") | |
| vargo build --features record-history | |
| ;; | |
| "no-std") | |
| vargo build --vstd-no-std | |
| cd vstd | |
| unset -f cargo | |
| cargo build --no-default-features --features alloc | |
| ;; | |
| "no-alloc") | |
| vargo build --vstd-no-std --vstd-no-alloc | |
| cd vstd | |
| unset -f cargo | |
| cargo build --no-default-features | |
| ;; | |
| esac | |
| - name: smoke test | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| case "${{ matrix.features }}" in | |
| "singular") | |
| hdiutil attach ../Singular-4-3-2_M1.dmg | |
| DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/Volumes/Singular4.3.2/Singular.app/Contents/lib VERUS_SINGULAR_PATH=/Volumes/Singular4.3.2/Singular.app/Contents/bin/Singular VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run -p air --features singular | |
| DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/Volumes/Singular4.3.2/Singular.app/Contents/lib VERUS_SINGULAR_PATH=/Volumes/Singular4.3.2/Singular.app/Contents/bin/Singular VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run -p rust_verify_test --features singular --test integer_ring | |
| DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/Volumes/Singular4.3.2/Singular.app/Contents/lib VERUS_SINGULAR_PATH=/Volumes/Singular4.3.2/Singular.app/Contents/bin/Singular VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run -p rust_verify_test --features singular --test examples -- examples_integer_ring | |
| ;; | |
| "record-history") | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run -p rust_verify_test --features record-history --test basic | |
| ;; | |
| esac | |
| # build the documentation | |
| # will complain if there are warnings | |
| build-docs: | |
| needs: [fmt, clippy] | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| - name: build docs | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| ./tools/get-z3.sh | |
| ./tools/docs.sh --strict # strict will complain if there are warnings | |
| - name: upload verusdoc artifact | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' && github.repository == 'verus-lang/verus' | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: verusdoc | |
| path: source/doc | |
| # build the release artifacts | |
| build-release: | |
| needs: [basic-test, smoke-test] | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' && github.repository == 'verus-lang/verus' | |
| strategy: | |
| matrix: | |
| build: [macos, macos-x86_64, linux, windows] | |
| include: | |
| - build: macos | |
| os: macos-14 | |
| release_name: verus-arm64-macos | |
| - build: macos-x86_64 | |
| os: macos-15-intel | |
| release_name: verus-x86-macos | |
| - build: linux | |
| os: ubuntu-22.04 | |
| release_name: verus-x86-linux | |
| - build: windows | |
| os: windows-2022 | |
| release_name: verus-x86-win | |
| runs-on: ${{ matrix.os }} | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: get z3 | |
| working-directory: ./source | |
| run: | | |
| ./tools/get-z3.sh | |
| echo z3 version `./z3 --version` | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.93.1 | |
| - name: build | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build --release | |
| - name: create archive | |
| working-directory: ./source | |
| run: | | |
| ./target-verus/release/verus --version --output-json > ./target-verus/release/version.json | |
| cp -R ./target-verus/release ../${{ matrix.release_name }} | |
| cd ..; | |
| if [ ${{ matrix.os }} == "windows-2022" ]; then | |
| 7z a ${{ matrix.release_name }}.zip ./${{ matrix.release_name }} | |
| else | |
| zip -r ${{ matrix.release_name }}.zip ./${{ matrix.release_name }} | |
| fi | |
| - name: upload release artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: ${{ matrix.release_name }} | |
| path: ${{ matrix.release_name }}.zip | |
| # upload the release artifacts | |
| release: | |
| needs: [build-docs, build-release, full-test] | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' && github.repository == 'verus-lang/verus' | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - name: download all artifacts | |
| uses: actions/download-artifact@v4 | |
| - name: create release tag | |
| shell: bash | |
| run: | | |
| cd verus-x86-linux; unzip verus-x86-linux.zip; cd .. | |
| echo "TAG_NAME=release/rolling/$(cat ./verus-x86-linux/verus-x86-linux/version.txt)" >> $GITHUB_ENV | |
| echo "RELEASE_NAME=$(cat ./verus-x86-linux/verus-x86-linux/version.txt)" >> $GITHUB_ENV | |
| echo $RELEASE_NAME $TAG_NAME | |
| - name: list artifacts | |
| run: ls -Al . | |
| - name: update release | |
| id: update_release | |
| uses: verus-lang/action-update-release@v0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| id: 163437062 | |
| new_name: Rolling Release ${{ env.RELEASE_NAME }} | |
| new_body: | | |
| Rolling release from Continuous Integration | |
| delete_tags_prefix: release/rolling/ | |
| delete_assets: true | |
| new_draft_status: true | |
| - name: upload release for x86-linux | |
| uses: actions/upload-release-asset@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.update_release.outputs.upload_url }} | |
| asset_path: ./verus-x86-linux/verus-x86-linux.zip | |
| asset_name: verus-${{ env.RELEASE_NAME }}-x86-linux.zip | |
| asset_content_type: application/zip | |
| - name: upload release for arm64-macos | |
| uses: actions/upload-release-asset@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.update_release.outputs.upload_url }} | |
| asset_path: ./verus-arm64-macos/verus-arm64-macos.zip | |
| asset_name: verus-${{ env.RELEASE_NAME }}-arm64-macos.zip | |
| asset_content_type: application/zip | |
| - name: upload release for x86-macos | |
| uses: actions/upload-release-asset@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.update_release.outputs.upload_url }} | |
| asset_path: ./verus-x86-macos/verus-x86-macos.zip | |
| asset_name: verus-${{ env.RELEASE_NAME }}-x86-macos.zip | |
| asset_content_type: application/zip | |
| - name: upload release for x86-win | |
| uses: actions/upload-release-asset@v1 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| upload_url: ${{ steps.update_release.outputs.upload_url }} | |
| asset_path: ./verus-x86-win/verus-x86-win.zip | |
| asset_name: verus-${{ env.RELEASE_NAME }}-x86-win.zip | |
| asset_content_type: application/zip | |
| - name: publish release | |
| uses: verus-lang/action-update-release@v0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| id: 163437062 | |
| new_tag: ${{ env.TAG_NAME }} | |
| new_draft_status: false |