Add fibonacci example to the Guide to illustrate how spec, proof, and exec code work together #6192
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] | |
| permissions: | |
| contents: write | |
| jobs: | |
| fmt: | |
| runs-on: macos-14 | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - 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 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 | |
| test-and-release-macos: | |
| runs-on: macos-14 | |
| strategy: | |
| matrix: | |
| features: ['', 'record-history', 'no-std', 'no-alloc', 'singular', 'cvc5'] | |
| 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 | |
| run: | | |
| curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y | |
| - 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 and test | |
| 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 | |
| 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 test -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 test -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 test -p rust_verify_test --features singular --test examples -- example_integer_ring | |
| ;; | |
| "record-history") | |
| vargo build --features record-history | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test --features record-history --test basic | |
| ;; | |
| "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 | |
| vargo run -p rust_verify -- -V cvc5 rust_verify/example/assorted_demo.rs | |
| ;; | |
| *) | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p air | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test | |
| cd vstd | |
| unset -f cargo | |
| cargo build | |
| ;; | |
| esac | |
| - name: build verus release | |
| if: matrix.features == '' | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build --release | |
| ./target-verus/release/verus --version --output-json > ./target-verus/release/version.json | |
| cp -R ./target-verus/release ../verus-arm64-macos | |
| cd ..; zip -r verus-arm64-macos.zip ./verus-arm64-macos | |
| - name: run verus release | |
| if: matrix.features == '' | |
| working-directory: ./source | |
| run: | | |
| ls -Al ./target-verus/release | |
| ./target-verus/release/verus ./rust_verify/example/test.rs | |
| - name: upload verus release artifact | |
| uses: actions/upload-artifact@v4 | |
| if: matrix.features == '' | |
| with: | |
| name: verus-arm64-macos | |
| path: verus-arm64-macos.zip | |
| - name: build docs | |
| if: matrix.features == '' | |
| working-directory: ./source | |
| run: | | |
| ./tools/docs.sh | |
| - name: upload verusdoc artifact | |
| uses: actions/upload-artifact@v4 | |
| if: matrix.features == '' | |
| with: | |
| name: verusdoc | |
| path: source/doc | |
| smoke-test-and-release-macos-x86: | |
| runs-on: macos-13 | |
| 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 | |
| run: | | |
| curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y | |
| - name: build and test | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test --test basic | |
| - name: build verus release | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build --release | |
| # TODO ./target-verus/release/verus --version --output-json > ./target-verus/release/version.json | |
| cp -R ./target-verus/release ../verus-x86-macos | |
| cd ..; zip -r verus-x86-macos.zip ./verus-x86-macos | |
| - name: run verus release | |
| working-directory: ./source | |
| run: | | |
| ls -Al ./target-verus/release | |
| ./target-verus/release/verus ./rust_verify/example/test.rs | |
| - name: upload verus release artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: verus-x86-macos | |
| path: verus-x86-macos.zip | |
| smoke-test-and-release-windows: | |
| runs-on: windows-latest | |
| steps: | |
| - name: checkout | |
| uses: actions/checkout@v4 | |
| - 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: build verus release | |
| working-directory: .\source | |
| run: | | |
| ../tools/activate.ps1 | |
| $env:VERUS_Z3_PATH = "$(Get-Location)\z3.exe"; vargo build --release | |
| # TODO: (currently fails misteriously) $env:VERUS_Z3_PATH = "$(Get-Location)/z3.exe"; ./target-verus/release/verus.exe --version --output-json > ./target-verus/release/version.json | |
| cp -R ./target-verus/release ../verus-x86-win | |
| cd ..; Compress-Archive -Path .\verus-x86-win -DestinationPath .\verus-x86-win.zip | |
| shell: powershell | |
| - name: run verus release | |
| working-directory: .\source | |
| run: | | |
| ls .\target-verus\release | |
| $env:VERUS_Z3_PATH = "$(Get-Location)\z3.exe"; Start-Process "$(Get-Location)\target-verus\release\verus.exe" "$(Get-Location)\rust_verify\example\test.rs" | |
| shell: powershell | |
| - name: upload verus release artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: verus-x86-win | |
| path: verus-x86-win.zip | |
| smoke-test-and-release-linux: | |
| runs-on: ubuntu-latest | |
| 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 | |
| run: | | |
| curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y | |
| - name: build and test | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build | |
| VERUS_Z3_PATH="$(pwd)/z3" vargo test -p rust_verify_test --test basic | |
| - name: build verus release | |
| working-directory: ./source | |
| run: | | |
| . ../tools/activate | |
| vargo clean | |
| vargo build --release | |
| # TODO ./target-verus/release/verus --version --output-json > ./target-verus/release/version.json | |
| cp -R ./target-verus/release ../verus-x86-linux | |
| cd ..; zip -r verus-x86-linux.zip ./verus-x86-linux | |
| - name: run verus release | |
| working-directory: ./source | |
| run: | | |
| ls -Al ./target-verus/release | |
| ./target-verus/release/verus ./rust_verify/example/test.rs | |
| - name: upload verus release artifact | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: verus-x86-linux | |
| path: verus-x86-linux.zip | |
| release: | |
| needs: [fmt, smoke-test-and-release-linux, smoke-test-and-release-windows, test-and-release-macos, smoke-test-and-release-macos-x86] | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| 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: utaal/action-update-release@v0.2 | |
| 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: utaal/action-update-release@v0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| with: | |
| id: 163437062 | |
| new_tag: ${{ env.TAG_NAME }} | |
| new_draft_status: false |