Improvements to multiset, map pervasives (#752) #4216
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 | |
| with: | |
| ref: ${{ github.event.pull_request && github.event.pull_request.head.sha || github.sha }} | |
| - 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'] | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v3 | |
| with: | |
| ref: ${{ github.event.pull_request && github.event.pull_request.head.sha || github.sha }} | |
| - 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 | |
| else | |
| vargo build | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p air | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test | |
| 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 | |
| with: | |
| ref: ${{ github.event.pull_request && github.event.pull_request.head.sha || github.sha }} | |
| - 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 | |
| shell: powershell |