Change Seq to an enum and verify its axioms #4929
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
| name: ci | |
| on: | |
| push: | |
| branches: | |
| - 'main' | |
| workflow_dispatch: | |
| pull_request: | |
| types: [opened, synchronize, reopened] | |
| jobs: | |
| fmt: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v3 | |
| - name: setup rust | |
| run: | | |
| curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y | |
| - name: check cargo fmt | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo fmt -- --check | |
| - name: check cargo fmt for vargo | |
| working-directory: ./tools/vargo | |
| run: | | |
| cargo fmt -- --check | |
| test: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| features: ['', 'singular', 'record-history'] | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v3 | |
| - name: get z3 | |
| working-directory: ./source | |
| run: | | |
| ../.github/workflows/get-z3.sh | |
| echo z3 version `./z3 --version` | |
| - name: setup rust | |
| run: | | |
| curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y | |
| - name: setup singular | |
| if: matrix.features == 'singular' | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y singular | |
| - name: cargo test | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| if [ "${{ matrix.features }}" == "singular" ]; then | |
| vargo build --features singular | |
| VERUS_Z3_PATH="$(pwd)/z3" VERUS_SINGULAR_PATH="/usr/bin/Singular" vargo test -p air --features singular | |
| VERUS_Z3_PATH="$(pwd)/z3" VERUS_SINGULAR_PATH="/usr/bin/Singular" vargo test -p rust_verify_test --features singular --test integer_ring | |
| VERUS_Z3_PATH="$(pwd)/z3" VERUS_SINGULAR_PATH="/usr/bin/Singular" vargo test -p rust_verify_test --features singular --test examples -- example_integer_ring | |
| elif [ "${{ matrix.features }}" == "record-history" ]; then | |
| vargo build --features record-history | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test --features record-history --test basic | |
| else | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p air | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test | |
| cd pervasive | |
| unset -f cargo | |
| cargo build | |
| cd .. | |
| fi | |
| - name: build docs | |
| if: matrix.features == '' | |
| working-directory: ./source | |
| run: | | |
| ./tools/docs.sh | |
| - name: upload artifact | |
| uses: actions/upload-artifact@v2 | |
| if: matrix.features == '' | |
| with: | |
| name: verusdoc | |
| path: source/doc | |
| smoke-test-windows: | |
| runs-on: windows-latest | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v3 | |
| - name: get z3 | |
| shell: pwsh | |
| working-directory: .\source | |
| run: | | |
| .\tools\get-z3.ps1 | |
| Write-Host "z3 version $(.\z3.exe --version)" | |
| - name: setup rust | |
| run: | | |
| # Disable the download progress bar which can cause perf issues | |
| $ProgressPreference = "SilentlyContinue" | |
| Invoke-WebRequest https://win.rustup.rs/ -OutFile rustup-init.exe | |
| .\rustup-init.exe -y --default-host=x86_64-pc-windows-msvc --default-toolchain=none | |
| del rustup-init.exe | |
| shell: powershell | |
| - name: cargo test | |
| working-directory: .\source | |
| run: | | |
| ../tools/activate.ps1 | |
| vargo clean | |
| vargo build | |
| $env:VERUS_Z3_PATH = "$(Get-Location)/z3"; vargo test -p rust_verify_test --test basic | |
| $env:VERUS_Z3_PATH = "$(Get-Location)/z3"; vargo test -p rust_verify_test --test layout | |
| shell: powershell |