CI #71
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] | |
| pull_request: | |
| workflow_dispatch: | |
| schedule: | |
| - cron: "0 6 * * 1" | |
| # The workflow only reads repository contents. Individual jobs do not receive | |
| # credentials beyond this unless they declare them explicitly. | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_INCREMENTAL: "0" | |
| CARGO_TERM_COLOR: always | |
| RUST_BACKTRACE: "1" | |
| VERUSFMT_VERSION: 0.7.2 | |
| MDBOOK_VERSION: 0.5.4 | |
| jobs: | |
| rust: | |
| name: Rust checks | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 45 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Read the pinned Rust version | |
| id: toolchain | |
| run: echo "rust=$(python3 -c 'import json; print(json.load(open("verus.json"))["rust"])')" >> "$GITHUB_OUTPUT" | |
| - uses: dtolnay/rust-toolchain@4cda84d5c5c54efe2404f9d843567869ab1699d4 # master | |
| with: | |
| toolchain: ${{ steps.toolchain.outputs.rust }} | |
| components: clippy, rustfmt | |
| - name: Restore Cargo cache | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry/index | |
| ~/.cargo/registry/cache | |
| ~/.cargo/git/db | |
| target | |
| key: ${{ runner.os }}-${{ runner.arch }}-rust-${{ steps.toolchain.outputs.rust }}-${{ hashFiles('Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-${{ runner.arch }}-rust-${{ steps.toolchain.outputs.rust }}- | |
| - name: Check formatting | |
| run: cargo fmt -p vest -p vest_asn1 -- --check | |
| - name: Run Clippy | |
| run: cargo clippy -p vest -p vest_asn1 --all-targets --locked | |
| - name: Run workspace tests | |
| run: cargo test --workspace --locked | |
| - name: Check vest_lib without allocation support | |
| run: cargo check -p vest_lib --no-default-features --all-targets --locked | |
| - name: Check vest_lib with alloc but without std | |
| run: cargo check -p vest_lib --no-default-features --features alloc --all-targets --locked | |
| - name: Check vest_lib documentation links | |
| env: | |
| RUSTDOCFLAGS: -D rustdoc::broken_intra_doc_links -D rustdoc::invalid_codeblock_attributes | |
| run: cargo doc -p vest_lib --no-deps --locked | |
| - name: Compile benchmarks with the workspace profile | |
| run: | | |
| cargo bench --no-run -p vest_tests -p vest_dev --locked 2>&1 | tee "$RUNNER_TEMP/bench-build.log" | |
| if grep -qi "profile.*non root package.*ignored" "$RUNNER_TEMP/bench-build.log"; then | |
| echo "A benchmark profile outside the workspace root was ignored." >&2 | |
| exit 1 | |
| fi | |
| regeneration: | |
| name: Generated files and guide | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 35 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Read the pinned Rust version | |
| id: toolchain | |
| run: echo "rust=$(python3 -c 'import json; print(json.load(open("verus.json"))["rust"])')" >> "$GITHUB_OUTPUT" | |
| - uses: dtolnay/rust-toolchain@4cda84d5c5c54efe2404f9d843567869ab1699d4 # master | |
| with: | |
| toolchain: ${{ steps.toolchain.outputs.rust }} | |
| components: rustfmt | |
| - name: Restore Cargo cache | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry/index | |
| ~/.cargo/registry/cache | |
| ~/.cargo/git/db | |
| target | |
| key: ${{ runner.os }}-${{ runner.arch }}-regen-${{ steps.toolchain.outputs.rust }}-${{ hashFiles('Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-${{ runner.arch }}-regen-${{ steps.toolchain.outputs.rust }}- | |
| - name: Restore documentation tools | |
| # Cache only version-pinned binaries; do not mix them into the Cargo cache. | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/bin/verusfmt | |
| ~/.cargo/bin/mdbook | |
| key: ${{ runner.os }}-${{ runner.arch }}-tools-verusfmt-${{ env.VERUSFMT_VERSION }}-mdbook-${{ env.MDBOOK_VERSION }} | |
| - name: Install exact generator tool versions | |
| run: | | |
| if [[ "$(verusfmt --version 2>/dev/null || true)" != "verusfmt ${VERUSFMT_VERSION}" ]]; then | |
| cargo install verusfmt --version "${VERUSFMT_VERSION}" --locked | |
| fi | |
| if [[ "$(mdbook --version 2>/dev/null || true)" != "mdbook v${MDBOOK_VERSION}" ]]; then | |
| cargo install mdbook --version "${MDBOOK_VERSION}" --locked | |
| fi | |
| - name: Regenerate Vest fixtures | |
| working-directory: vest_tests | |
| run: make vest | |
| - name: Check rejected Vest fixtures | |
| working-directory: vest_tests | |
| run: make bad | |
| - name: Test Vest snippets in the guide | |
| run: cargo test -p vest_guide_tests --locked | |
| - name: Regenerate ASN.1 fixtures | |
| working-directory: vest_asn1_tests | |
| run: make generate | |
| - name: Build and test the guide | |
| run: scripts/build-guide.sh && mdbook test | |
| - name: Check that generated files are current | |
| run: | | |
| git diff --exit-code | |
| untracked="$(git ls-files --others --exclude-standard)" | |
| if [[ -n "$untracked" ]]; then | |
| echo "Generation produced untracked files:" >&2 | |
| printf '%s\n' "$untracked" >&2 | |
| exit 1 | |
| fi | |
| verus-linux: | |
| name: Prepare pinned Verus | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 20 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Restore pinned Verus | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: .verus | |
| key: verus-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('verus.json', 'scripts/install-verus.sh') }} | |
| - name: Install and validate pinned Verus | |
| run: scripts/install-verus.sh | |
| verify: | |
| name: Verify ${{ matrix.name }} | |
| needs: verus-linux | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 90 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - name: vest_lib-core | |
| cargo_args: -p vest_lib --no-default-features | |
| verus_args: --expand-errors | |
| - name: vest_lib-alloc | |
| cargo_args: -p vest_lib --no-default-features --features alloc | |
| verus_args: --expand-errors | |
| - name: vest_lib-std | |
| cargo_args: -p vest_lib | |
| verus_args: --expand-errors | |
| - name: vest-tests | |
| cargo_args: -p vest_tests | |
| verus_args: --expand-errors | |
| # This matches vest_asn1_tests/Makefile. The width stress fixture needs | |
| # more SMT budget than the Verus default. | |
| - name: vest-asn1-tests | |
| cargo_args: -p vest_asn1_tests | |
| verus_args: --expand-errors --rlimit 100 | |
| - name: vest-dev | |
| cargo_args: -p vest_dev | |
| verus_args: --expand-errors | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Restore pinned Verus | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: .verus | |
| key: verus-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('verus.json', 'scripts/install-verus.sh') }} | |
| - name: Install pinned Verus and Rust toolchain | |
| run: scripts/install-verus.sh | |
| - name: Add Verus to PATH | |
| run: echo "${{ github.workspace }}/.verus" >> "$GITHUB_PATH" | |
| - name: Restore Cargo downloads | |
| # Deliberately do not cache target/: cached Verus artifacts can cause | |
| # verification conditions to be skipped as already fresh. | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry/index | |
| ~/.cargo/registry/cache | |
| ~/.cargo/git/db | |
| key: ${{ runner.os }}-${{ runner.arch }}-verus-cargo-${{ hashFiles('Cargo.lock', 'verus.json') }} | |
| restore-keys: | | |
| ${{ runner.os }}-${{ runner.arch }}-verus-cargo- | |
| - name: Verify ${{ matrix.name }} | |
| env: | |
| CARGO_ARGS: ${{ matrix.cargo_args }} | |
| VERUS_ARGS: ${{ matrix.verus_args }} | |
| run: | | |
| # A new target directory guarantees that this job checks the current | |
| # verification conditions rather than restored Cargo freshness data. | |
| cargo verus verify ${CARGO_ARGS} --locked --check-toolchain \ | |
| --target-dir "$RUNNER_TEMP/verus-target" -- ${VERUS_ARGS} | |
| verify-macos: | |
| name: Verify supported packages on macOS | |
| if: github.event_name == 'schedule' | |
| runs-on: macos-15 | |
| timeout-minutes: 150 | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| persist-credentials: false | |
| - name: Restore pinned Verus | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: .verus | |
| key: verus-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('verus.json', 'scripts/install-verus.sh') }} | |
| - name: Install pinned Verus and Rust toolchain | |
| run: scripts/install-verus.sh | |
| - name: Add Verus to PATH | |
| run: echo "${{ github.workspace }}/.verus" >> "$GITHUB_PATH" | |
| - name: Restore Cargo downloads | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cargo/registry/index | |
| ~/.cargo/registry/cache | |
| ~/.cargo/git/db | |
| key: ${{ runner.os }}-${{ runner.arch }}-verus-cargo-${{ hashFiles('Cargo.lock', 'verus.json') }} | |
| restore-keys: | | |
| ${{ runner.os }}-${{ runner.arch }}-verus-cargo- | |
| - name: Verify vest_lib | |
| run: cargo verus verify -p vest_lib --locked --check-toolchain --target-dir "$RUNNER_TEMP/verus-target" -- --expand-errors | |
| - name: Verify Vest fixtures | |
| run: cargo verus verify -p vest_tests --locked --check-toolchain --target-dir "$RUNNER_TEMP/verus-target" -- --expand-errors | |
| - name: Verify ASN.1 fixtures | |
| run: cargo verus verify -p vest_asn1_tests --locked --check-toolchain --target-dir "$RUNNER_TEMP/verus-target" -- --expand-errors --rlimit 100 | |
| - name: Verify development formats | |
| run: cargo verus verify -p vest_dev --locked --check-toolchain --target-dir "$RUNNER_TEMP/verus-target" -- --expand-errors |