Skip to content

Split further

Split further #29

Workflow file for this run

name: Run evaluation
on:
push:
branches: [cav-eval]
workflow_dispatch:
jobs:
eval:
strategy:
fail-fast: false
matrix:
verifier:
- name: 'carbon'
args: 'lt carbon/silver/src/test/resources/capture_avoidance/'
tag: '-1'
- name: 'carbon'
args: 'ge carbon/silver/src/test/resources/capture_avoidance/'
tag: '-2'
- name: 'dafny'
args: 'lt dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/11-'
tag: '-1'
- name: 'dafny'
args: 'in dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/11- dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/'
tag: '-2'
- name: 'dafny'
args: 'ge dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/'
tag: '-3'
- name: 'fstar'
args: 'lt fstar/examples/'
tag: '-1'
- name: 'fstar'
args: 'ge fstar/examples/'
tag: '-2'
- name: 'silicon'
- name: 'smt-comp'
args: 'lt smt-comp/incremental/QF_BVLRA/20240414-mapf_r/soc/coef_2/'
tag: '-1'
- name: 'smt-comp'
args: 'in smt-comp/incremental/QF_BVLRA/20240414-mapf_r/soc/coef_2/ smt-comp/non-incremental/QF_SLIA/'
tag: '-2'
- name: 'smt-comp'
args: 'ge smt-comp/non-incremental/QF_SLIA/'
tag: '-3'
- name: 'verus'
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
submodules: 'recursive'
- name: Install Z3
uses: pavpanchekha/[email protected]
with:
version: '4.8.7'
- name: Cache cargo
uses: Swatinem/rust-cache@v2
with:
shared-key: "shared"
save-if: "false"
- run: ./eval/build.sh
- run: ./eval/eval.sh ${{ matrix.verifier.name }} ${{ matrix.verifier.args }}
- name: Archive data for upload
if: always()
run: tar -czf ${{ matrix.verifier.name }}${{ matrix.verifier.tag }}.tar.bz2 eval/data/${{ matrix.verifier.name }}
- uses: actions/[email protected]
if: always()
with:
name: "${{ matrix.verifier.name }}${{ matrix.verifier.tag }}"
path: ${{ matrix.verifier.name }}${{ matrix.verifier.tag }}.tar.bz2
retention-days: 30