GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-10-06 00:22:49 +03:00
Code Issues Projects Releases Wiki Activity

[CI] Add STP solver versions to testing matrix.

Browse Source
This commit is contained in:
Kevin Quick 2022-01-12 20:18:06 -08:00
parent b8389562b5
commit 223831a817
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 45 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
.github/workflows/test.yml vendored
View File

@ -28,7 +28,7 @@ env:
jobs:
linux:
name: GHC-${{ matrix.ghc }} Z3-${{ matrix.z3 }} Yices-${{ matrix.yices }} CVC4-${{ matrix.cvc4 }} ${{ matrix.os }}
name: GHC-${{ matrix.ghc }} Z3-${{ matrix.z3 }} Yices-${{ matrix.yices }} CVC4-${{ matrix.cvc4 }} STP-${{ matrix.stp }} ${{ matrix.os }}
runs-on: ${{ matrix.os }}
continue-on-error: ${{ matrix.allow-failure }}
env:
@ -39,6 +39,7 @@ jobs:
ghc: [9.0.2, 8.10.7, 8.8.4, 8.6.5]
z3: [ 4_8_14 ]
yices: [ 2_6 ]
stp: [ 2_3_3 ]
cvc4: [ 1_8 ]
allow-failure: [ false ]
# Specify multiple older solver versions for the latest builds
@ -52,35 +53,41 @@ jobs:
ghc: 9.0.2
cvc4: 1_8
z3: 4_8_8
stp: 2_3_3
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_9
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_10
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_11
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_12
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_13
yices: 2_6
allow-failure: false
@ -88,12 +95,14 @@ jobs:
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_14
yices: 2_6_1
allow-failure: false
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_8
stp: 2_3_3
z3: 4_8_14
yices: 2_5
allow-failure: true
@ -101,44 +110,60 @@ jobs:
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_7
stp: 2_3_3
z3: 4_8_14
yices: 2_6
allow-failure: false
### STP variations ----------
- os: ubuntu-latest
ghc: 9.0.2
cvc4: 1_7
stp: 2_3_2
z3: 4_8_14
yices: 2_6
allow-failure: false
# STP 2_2_0 fails: no reason to test it
## GHC 8.10.7 ------------------------------
### Z3 variations ----------
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_8
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_9
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_10
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_11
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_12
yices: 2_6
allow-failure: false
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_13
yices: 2_6
allow-failure: false
@ -146,12 +171,14 @@ jobs:
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_14
yices: 2_6_1
allow-failure: false
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_8
stp: 2_3_3
z3: 4_8_14
yices: 2_5
allow-failure: true
@ -159,9 +186,19 @@ jobs:
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_7
stp: 2_3_3
z3: 4_8_14
yices: 2_6
allow-failure: false
### STP variations ----------
- os: ubuntu-latest
ghc: 8.10.7
cvc4: 1_7
stp: 2_3_2
z3: 4_8_14
yices: 2_6
allow-failure: false
# STP 2_2_0 fails: no reason to test it
fail-fast: false
steps:
- uses: actions/checkout@v2
@ -262,10 +299,15 @@ jobs:
cd what4
echo Boolector version $(nix eval nixpkgs#boolector.version)
echo CVC4 version $(nix run github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} -- --version | head -n1)
echo STP version $(nix eval nixpkgs#stp.version)
echo STP version $(nix run github:GaloisInc/flakes#stp.v${{ matrix.stp }} -- --version)
echo Yices version $(nix run github:GaloisInc/flakes#yices.v${{ matrix.yices }} -- --version | head -n1)
echo Z3 version $(nix run github:GaloisInc/flakes#z3.v${{ matrix.z3 }} -- --version | head -n1)
$NS nixpkgs#abc-verifier nixpkgs#boolector github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} nixpkgs#stp github:GaloisInc/flakes#yices.v${{ matrix.yices }} github:GaloisInc/flakes#z3.v${{ matrix.z3 }} -c cabal test
$NS nixpkgs#abc-verifier nixpkgs#boolector \
github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} \
github:GaloisInc/flakes#stp.v${{ matrix.stp }} \
github:GaloisInc/flakes#yices.v${{ matrix.yices }} \
github:GaloisInc/flakes#z3.v${{ matrix.z3 }} \
-c cabal test
- name: Documentation
shell: bash