Skip to content

Prover Test

Prover Test #1912

Workflow file for this run

name: "Prover Test"
on:
# TODO enable this when we have time
# pull_request:
# paths:
# - '**.move'
# - 'aptos-move/move-deps/Cargo.toml'
# push:
# branches:
# - main
# - devnet
# - testnet
# - auto
# - canary
# paths:
# - '**.move'
# - 'aptos-move/move-deps/Cargo.toml'
# Allow triggering manually
workflow_dispatch:
# Until enabled on all PRs, run continuously at the beginning of each hour
schedule:
- cron: "0 * * * *"
env:
HAS_BUILDPULSE_SECRETS: ${{ secrets.BUILDPULSE_ACCESS_KEY_ID != '' && secrets.BUILDPULSE_SECRET_ACCESS_KEY != '' }}
HAS_DATADOG_SECRETS: ${{ secrets.DD_API_KEY != '' }}
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:
# TODO add determinator step to only run on move files
prover-test:
runs-on: high-perf-docker
steps:
- uses: actions/checkout@93ea575cb5d8a053eaa0ac8fa3b40d7e05a33cc8 # pin@v3
with:
fetch-depth: 0 # get all the history because cargo xtest --change-since origin/main requires it.
- uses: ./.github/actions/rust-setup
- name: install Prover dependencies
shell: bash
run: scripts/dev_setup.sh -b -p -y
- 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: cargo test -p move-examples --release -- --include-ignored prover
- run: cargo test -p framework --release -- --include-ignored prover