regression-testing.yml

name: Regression Testing
run-name: Regression tests run by ${{ github.actor }}
on:
  push:
    branches:
      - main
    paths-ignore:
      - "README.md"
      - ".gitignore"
      - "doc/**"
  pull_request:
  workflow_dispatch:
jobs:
  regression-testing:
    runs-on: ubuntu-20.04
    steps:
      - uses: actions/checkout@v2
      - name: Download Verus
        uses: actions/checkout@v2
        with:
          repository: verus-lang/verus
          path: verus
      - name: Install Rust toolchain
        run: |
          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y
      - name: Build Verus
        run: |
          cd verus/source
          ./tools/get-z3.sh
          source ../tools/activate
          vargo build --release
      - name: Build main and run unit tests
        run: |
          VERUS_DIR=$PWD/verus ./build.sh main.rs --time
          src/main
      - name: Build simple controller
        run: VERUS_DIR=$PWD/verus ./build.sh simple_controller.rs --rlimit 30 --time
      - name: Build zookeeper controller
        run: VERUS_DIR=$PWD/verus ./build.sh zookeeper_controller.rs --rlimit 30 --time
      - name: Build rabbitmq controller
        run: VERUS_DIR=$PWD/verus ./build.sh rabbitmq_controller.rs --rlimit 30 --time
      - name: Build fluent controller
        run: VERUS_DIR=$PWD/verus ./build.sh fluent_controller.rs --rlimit 30 --time