prover-daily-test.yaml

name: "Prover Daily Test"
on:
  # Allow us to manually run this specific workflow without a PR
  workflow_dispatch:
  # Until enabled on all PRs, run twice a week
  schedule:
    - cron: "14 14 */3 * *"

env:
  CARGO_INCREMENTAL: "0"
  CARGO_TERM_COLOR: always

# cancel redundant builds
concurrency:
  # cancel redundant builds on PRs (only on PR, not on branches)
  group: ${{ github.workflow }}-${{ (github.event_name == 'pull_request' && github.ref) || github.sha }}
  cancel-in-progress: true

jobs:
  prover-inconsistency-test:
    runs-on: high-perf-docker
    steps:
      - uses: actions/checkout@v3
        with:
          fetch-depth: 0 # get all the history because cargo xtest --change-since origin/main requires it.
      - uses: aptos-labs/aptos-core/.github/actions/rust-setup@main
      - name: install Prover dependencies
        shell: bash
        run: scripts/dev_setup.sh -b -p -y -J
      - name: prepare move lang prover tooling.
        shell: bash
        run: |
          echo 'Z3_EXE='/home/runner/bin/z3 | tee -a $GITHUB_ENV
          echo 'CVC5_EXE='/home/runner/bin/cvc5 | tee -a $GITHUB_ENV
          echo 'DOTNET_ROOT='/home/runner/.dotnet/ | tee -a $GITHUB_ENV
          echo 'BOOGIE_EXE='/home/runner/.dotnet/tools/boogie | tee -a $GITHUB_ENV
          echo 'MVP_TEST_ON_CI'='1' | tee -a $GITHUB_ENV
          echo "/home/runner/bin" | tee -a $GITHUB_PATH
          echo "/home/runner/.dotnet" | tee -a $GITHUB_PATH
          echo "/home/runner/.dotnet/tools" | tee -a $GITHUB_PATH
      - run: MVP_TEST_DISALLOW_TIMEOUT_OVERWRITE=1 MVP_TEST_VC_TIMEOUT=1200 cargo test -p aptos-move-examples --release -- --include-ignored prover
      - run: MVP_TEST_DISALLOW_TIMEOUT_OVERWRITE=1 MVP_TEST_VC_TIMEOUT=1200 cargo test -p aptos-framework --release -- --include-ignored prover
      - run: MVP_TEST_DISALLOW_TIMEOUT_OVERWRITE=1 MVP_TEST_VC_TIMEOUT=1200 MVP_TEST_INCONSISTENCY=1 cargo test -p aptos-move-examples --release -- --include-ignored prover
      - run: MVP_TEST_DISALLOW_TIMEOUT_OVERWRITE=1 MVP_TEST_VC_TIMEOUT=1200 MVP_TEST_INCONSISTENCY=1 cargo test -p aptos-framework --release -- --include-ignored prover