Skip to content
ci

Add specifications for vstd::vec #11316

Sign in to view logs

Add specifications for vstd::vec

Add specifications for vstd::vec #11316

Workflow file for this run

.github/workflows/ci.yml at bc667c0
name: ci
on:
workflow_dispatch:
merge_group:
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-refs/pull/<PR #>/merge (in the case of PRs) and
# ci-refs/heads/gh-readonly-queue/main/pr-<N>-<sha> for merge queue executions
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
permissions:
contents: write
jobs:
# check if formatting is correct
fmt:
runs-on: ubuntu-24.04
steps:
- name: checkout
uses: actions/checkout@v6
- name: setup rust
uses: dtolnay/rust-toolchain@master
with:
toolchain: 1.97.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: |
cargo fmt -- --check
# TODO: Should use `cargo verus fmt` when it's implemented:
# https://github.com/verus-lang/verus/issues/2758
find ./vstd -name '*.rs' -type f -exec verusfmt --check {} +
- name: check cargo fmt for vargo
working-directory: ./tools/vargo
run: cargo fmt -- --check
# run linter (clippy)
clippy:
runs-on: ubuntu-24.04
steps:
- name: checkout
uses: actions/checkout@v6
- name: setup rust
uses: dtolnay/rust-toolchain@master
with:
toolchain: 1.97.1
components: clippy
- name: clippy check codebase
working-directory: ./source
run: cargo clippy -- -D warnings
- name: clippy check vargo
working-directory: ./tools/vargo
run: cargo clippy -- -D warnings
# smoke test toolchain manifest creation
create-manifest-smoke-test:
runs-on: ubuntu-24.04
steps:
- name: checkout
uses: actions/checkout@v6
- name: setup rust
uses: dtolnay/rust-toolchain@master
with:
toolchain: 1.96.0
- name: smoke test create-manifest
working-directory: ./source
run: |
cargo run -p cargo-verus-toolchains --bin create-manifest -- --write-to-dir cargo-verus/toolchain-manifests
cargo run -p cargo-verus-toolchains --bin create-manifest -- --rolling --write-to-dir cargo-verus/toolchain-manifests
# detect whether subprojects (e.g. cargo-verus) changed
change_filter:
runs-on: ubuntu-24.04
outputs:
cargo_verus: ${{ steps.filter.outputs.cargo_verus }}
steps:
- name: checkout
uses: actions/checkout@v6
with:
fetch-depth: 0
- name: detect changed paths
id: filter
uses: dorny/paths-filter@v4
with:
filters: |
cargo_verus:
- 'source/cargo-verus/**'
- 'source/cargo-verus-toolchains/**'
# run cargo-verus tests
cargo-verus-test:
needs: [fmt, clippy, change_filter]
runs-on: ubuntu-24.04
steps:
- name: check for cargo-verus changes
if: needs.change_filter.outputs.cargo_verus != 'true'
run: echo "No source/cargo-verus changes detected; skipping cargo-verus tests."
- name: checkout
if: needs.change_filter.outputs.cargo_verus == 'true'
uses: actions/checkout@v6
- name: setup rust
if: needs.change_filter.outputs.cargo_verus == 'true'
uses: dtolnay/rust-toolchain@master
with:
toolchain: 1.97.1
- name: cargo-verus tests
if: needs.change_filter.outputs.cargo_verus == 'true'
working-directory: ./source
run: cargo test -p cargo-verus
# run line_count tests
line-count-test:
needs: [fmt, clippy]
runs-on: ubuntu-24.04
steps:
- name: checkout
uses: actions/checkout@v6
- name: setup rust
uses: dtolnay/rust-toolchain@master
with:
toolchain: 1.97.1
- name: setup nextest
uses: taiki-e/install-action@nextest
- name: line_count tests
working-directory: ./source/tools/line_count
run: cargo nextest run
# 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@v6
- 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.97.1
- name: setup nextest
uses: taiki-e/install-action@nextest
- name: build
working-directory: ./source
run: |
cargo clean
CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo build --release
cargo run --release -p cargo-verus -- build --release --manifest-path vstd/Cargo.toml
- name: full tests
working-directory: ./source
run: |
# check cvc5
cargo run --release -p rust_verify -- -V cvc5 ../examples/assorted_demo.rs
CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo nextest run --release -p air
CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo nextest run --release -p rust_verify_test
# 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-24.04
- build: windows
os: windows-2022
runs-on: ${{ matrix.os }}
defaults:
run:
shell: bash
steps:
- name: checkout
uses: actions/checkout@v6
- 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.97.1
- name: setup nextest
uses: taiki-e/install-action@nextest
- name: build
working-directory: ./source
run: |
cargo clean
cargo build
cargo run -p cargo-verus -- build --manifest-path vstd/Cargo.toml
- name: basic tests
working-directory: ./source
run: |
cargo nextest run -p rust_verify_test --test basic
# 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@v6
- 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.97.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: |
cargo 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 cargo build --features singular
cargo run -p cargo-verus -- build --manifest-path vstd/Cargo.toml
;;
"record-history")
cargo build --features record-history
cargo run -p cargo-verus -- build --manifest-path vstd/Cargo.toml
;;
"no-std")
cargo build
cargo run -p cargo-verus -- build --manifest-path vstd/Cargo.toml --no-default-features --features alloc
cd .. # important to disable the source/.cargo/config.toml
cargo build --manifest-path source/vstd/Cargo.toml --no-default-features --features alloc
;;
"no-alloc")
cargo build
cargo run -p cargo-verus -- build --manifest-path vstd/Cargo.toml --no-default-features
cd .. # important to disable the source/.cargo/config.toml
cargo build --manifest-path source/vstd/Cargo.toml --no-default-features
;;
esac
- name: smoke test
working-directory: ./source
run: |
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 cargo 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 cargo 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 cargo nextest run -p rust_verify_test --features singular --test examples -- examples_integer_ring
;;
"record-history")
cargo 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-24.04
steps:
- name: checkout
uses: actions/checkout@v6
- name: setup rust
uses: dtolnay/rust-toolchain@master
with:
toolchain: 1.97.1
- name: build docs
working-directory: ./source
run: |
./tools/get-z3.sh
./tools/docs-cargo.sh --strict # strict will complain if there are warnings