ci.yml

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