Skip to content

[test] Runtimes separation #478

[test] Runtimes separation

[test] Runtimes separation #478

Workflow file for this run

name: formal verification
on:
push:
tags:
- "[0-9]+.[0-9]+.[0-9]+"
- "[0-9]+.[0-9]+.[0-9]+-rc.[0-9]+"
branches: ["*"]
pull_request:
types:
- opened
- synchronize
branches:
- "release**"
- "main**"
env:
DOTNET_ROOT: "/home/github-runner/.dotnet"
Z3_EXE: "/home/github-runner/bin/z3"
CVC5_EXE: "/home/github-runner/bin/cvc5"
BOOGIE_EXE: "/home/github-runner/.dotnet/tools/boogie"
SOLC_EXE: "/home/github-runner/bin/solc"
jobs:
formal:
runs-on: debian-latest
steps:
# # NOTE: for debugging CI this allow shell access to github runner. Will print out tmate.io terminal url
# - name: Setup tmate session
# uses: mxschmitt/action-tmate@v3
# with:
# detached: true
# timeout-minutes: 15
- uses: actions/checkout@v3
- name: setup env
uses: ./.github/actions/build_env
- uses: Swatinem/[email protected]
with:
shared-key: "libra-framework"
cache-all-crates: true
- name: install prover dependencies
run: |
bash util/dev_setup.sh -byp
- name: install diem (for move tests)
run: |
wget -O ${{github.workspace}}/diem https://github.com/0LNetworkCommunity/diem/releases/latest/download/diem &&
chmod +x ${{github.workspace}}/diem &&
cp ${{github.workspace}}/diem ~/.cargo/bin
# Move framework tests
# TODO:
- name: prover tests
working-directory: ./framework
run: make prove