Skip to content

belolourenco setting up environment #110

belolourenco setting up environment

belolourenco setting up environment #110

name: replay-why3-proofs
run-name: ${{ github.actor }} setting up environment
on: [push]
env:
CVC4_URL: "https://github.com/CVC4/CVC4-archived/releases/download/1.8/cvc4-1.8-x86_64-linux-opt"
CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.3/cvc5-Linux"
Z3_URL: "https://github.com/Z3Prover/z3/releases/download/z3-4.11.2/z3-4.11.2-x64-glibc-2.31.zip"
jobs:
install-and-test:
runs-on: ubuntu-latest
steps:
- name: Check out repository code
uses: actions/checkout@v4
- name: Use OCaml
uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: 4.13.x
- name: install tools with opam
run: |
opam update
opam install why3.1.7.2
# install both alt-ergo 2.4.2 and alt-ergo 2.5.3
opam install alt-ergo.2.4.2
# install both eprover-2.6 and eprover-3.0
opam install eprover.2.6
eval $(opam env)
cp $(which alt-ergo) $(which alt-ergo)-2.4.2
cp $(which eprover) $(which eprover)-2.6
opam install alt-ergo.2.5.3
opam install eprover.3.0
eval $(opam env)
cp $(which alt-ergo) $(which alt-ergo)-2.5.3
cp $(which eprover) $(which eprover)-3.0
- name: download z3, cvc4, and cvc5
run: |
mkdir downloads
cd downloads
wget $CVC4_URL
chmod +x ${CVC4_URL##*/}
mv ${CVC4_URL##*/} /usr/local/bin/cvc4
wget $CVC5_URL
chmod +x ${CVC5_URL##*/}
mv ${CVC5_URL##*/} /usr/local/bin/cvc5
wget $Z3_URL
z3folder=${Z3_URL##*/}
unzip $z3folder
mv ${z3folder%.*}/bin/z3 /usr/local/bin
- name: test installation
run: |
eval $(opam env)
tools=(why3 alt-ergo-2.4.2 alt-ergo-2.5.3 eprover-2.6 eprover-3.0 z3 cvc4 cvc5)
for tool in ${tools[@]}; do
cmd="which ${tool}"
echo $cmd
eval $cmd
cmd="${tool} --version"
echo $cmd
eval $cmd
done
- name: replay proofs
run: |
echo "eval $(opam env)"
eval $(opam env)
echo "why3 config detect"
why3 config detect
echo "why3 config list-provers"
why3 config list-provers
echo "cd $GITHUB_WORKSPACE"
cd $GITHUB_WORKSPACE
echo "# Replay Status" > $GITHUB_STEP_SUMMARY
echo "./test.sh"
./test.sh