ci: refactor for maintainability and optimize for latency #8100
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] | |
| permissions: | |
| contents: write | |
| jobs: | |
| fmt: | |
| runs-on: macos-14 | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.91.0 | |
| - 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 | |
| docs: | |
| runs-on: macos-14 | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - name: setup rust | |
| uses: dtolnay/rust-toolchain@master | |
| with: | |
| toolchain: 1.91.0 | |
| - name: check rustdoc | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| ./tools/get-z3.sh | |
| ./tools/docs.sh --check | |
| test: | |
| strategy: | |
| matrix: | |
| build: [macos, macos-x86_64, macos-record-history, macos-no-std, macos-no-alloc, macos-singular, macos-cvc5, linux, windows] | |
| include: | |
| - build: macos | |
| os: macos-14 | |
| features: '' | |
| release_name: verus-arm64-macos | |
| - build: macos-x86_64 | |
| os: macos-15-intel | |
| features: '' | |
| release_name: verus-x86-macos | |
| - build: macos-record-history | |
| os: macos-14 | |
| features: 'record-history' | |
| - build: macos-no-std | |
| os: macos-14 | |
| features: 'no-std' | |
| - build: macos-no-alloc | |
| os: macos-14 | |
| features: 'no-alloc' | |
| - build: macos-singular | |
| os: macos-14 | |
| features: 'singular' | |
| - build: macos-cvc5 | |
| os: macos-14 | |
| features: 'cvc5' | |
| - build: linux | |
| os: ubuntu-latest | |
| features: '' | |
| release_name: verus-x86-linux | |
| - build: windows | |
| os: windows-latest | |
| features: '' | |
| 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.91.0 | |
| - name: setup nextest | |
| uses: taiki-e/install-action@nextest | |
| - name: download singular | |
| if: matrix.features == 'singular' | |
| run: curl -LO https://www.singular.uni-kl.de/ftp/pub/Math/Singular/UNIX/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 --release --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 | |
| ;; | |
| "cvc5") | |
| ./tools/get-cvc5.sh | |
| echo cvc5 version `./cvc5 --version` | |
| vargo build --release | |
| ;; | |
| *) | |
| vargo build --release | |
| # build zip file with release if we're not on a fork | |
| if [ ${{ github.repository }} == 'verus-lang/verus' ]; then | |
| ./target-verus/release/verus --version --output-json > ./target-verus/release/version.json | |
| cp -R ./target-verus/release ../${{ matrix.release_name }} | |
| cd ..; zip -r ${{ matrix.release_name }}.zip ./${{ matrix.release_name }} | |
| cd ./source | |
| fi | |
| esac | |
| - name: 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 --release -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 --release -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 --release -p rust_verify_test --features singular --test examples -- examples_integer_ring | |
| ;; | |
| "record-history") | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run --release -p rust_verify_test --features record-history --test basic | |
| ;; | |
| "no-alloc") | |
| ;; | |
| "no-std") | |
| ;; | |
| "cvc5") | |
| vargo run --release -p rust_verify -- -V cvc5 ../examples/assorted_demo.rs | |
| ;; | |
| *) | |
| if [ ${{ matrix.build }} == "macos" ]; then | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run --release -p air | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run --release -p rust_verify_test | |
| cd vstd | |
| unset -f cargo | |
| cargo build | |
| else | |
| # run only the basic tests (we only fully test on macos) | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo nextest run --release -p rust_verify_test --test basic | |
| fi | |
| ;; | |
| esac | |
| - name: build line-count tool | |
| if: matrix.features == '' | |
| working-directory: ./source/tools/line_count | |
| run: cargo build | |
| - name: upload verus release artifact | |
| uses: actions/upload-artifact@v4 | |
| if: github.repository == 'verus-lang/verus' && matrix.release_name != '' | |
| with: | |
| name: ${{ matrix.release_name }} | |
| path: ${{ matrix.release_name }}.zip | |
| build-docs: | |
| needs: [fmt, docs] | |
| runs-on: macos-14 | |
| if: github.repository == 'verus-lang/verus' | |
| steps: | |
| - name: build docs | |
| working-directory: ./source | |
| run: ./tools/docs.sh | |
| - name: upload verusdoc artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: verusdoc | |
| path: source/doc | |
| release: | |
| needs: [build-docs, test] | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' && github.repository == 'verus-lang/verus' | |
| runs-on: ubuntu-latest | |
| 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/[email protected] | |
| 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/[email protected] | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| id: 163437062 | |
| new_tag: ${{ env.TAG_NAME }} | |
| new_draft_status: false |