Commit 662d5c1c authored by François Bobot's avatar François Bobot

[CI] adds a small parts of nightly bench

     - only some examples (examples/reduced_regtests.list)
     - only some provers
     - update ocaml version used for alt-ergo 2.0.0
parent 5fc911ca
stages:
- build
- test
- nightly
- deploy
.build_template: &build_definition
......@@ -41,7 +42,8 @@ build-4.07.0:
bench:
stage: test
variables:
COMPILER: system
COMPILER: 4.04.0
OPAM_PACKAGES: alt-ergo.2.0.0
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
......@@ -81,12 +83,21 @@ bench-4.07.0:
full:
stage: test
variables:
COMPILER: system
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra
OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx
COMPILER: 4.04.0
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra lmodern texlive-fonts-recommended
OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx alt-ergo.2.0.0
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide doc
nightly-bench:
stage: nightly
variables:
COMPILER: 4.04.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.1 coq-flocq.2.6.1
script:
- misc/ci-docker.sh misc/ci-local.sh nightly-bench-reduced
opam:
stage: build
variables:
......
counting_sort
leftist_heap
binary_sort
mergesort_array
#!/bin/sh
#!/bin/sh -eu
# regression tests for why3
REPLAYOPT=""
REGTESTS_MODE=""
while test $# != 0; do
case "$1" in
......@@ -15,6 +16,9 @@ case "$1" in
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
"--reduced-mode")
REGTESTS_MODE="REDUCED"
;;
*)
echo "$0: Unknown option '$1'"
exit 2
......@@ -39,12 +43,24 @@ export shapes=""
run_dir () {
for f in `ls $1/*/why3session.xml`; do
if [ "$REGTESTS_MODE" = "REDUCED" ]; then
if [ -f $1/reduced_regtests.list ]; then
LIST=`sed $1/reduced_regtests.list -e "s&.*&$1/\0/why3session.xml&"`
else
LIST=
fi
else
LIST=`ls $1/*/why3session.xml`
fi
for f in $LIST; do
d=`dirname $f`
printf "Replaying $d ... "
../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
ret=$?
if test "$ret" != "0" ; then
if ../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP ; then
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
else
ret=$?
printf "FAILED (ret code=$ret):"
out=`head -1 $TMP`
if test -z "$out" ; then
......@@ -54,10 +70,6 @@ run_dir () {
cat $TMP
fi
res=1
else
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
fi
total=`expr $total + 1`
done
......@@ -67,13 +79,13 @@ run_dir () {
echo "=== Programs already ported === MUST REPLAY AND ALL GOALS PROVED ==="
echo ""
run_dir .
run_dir . ""
run_dir double_wp "-L double_wp"
run_dir avl "-L avl"
run_dir foveoos11-cm
run_dir foveoos11-cm ""
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multiplication"
run_dir WP_revisited
run_dir WP_revisited ""
run_dir prover "-L prover --debug ignore_unused_vars"
run_dir multiprecision "-L multiprecision"
echo ""
......
......@@ -8,6 +8,20 @@ ARG debian_packages
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove && apt-get install -yq --no-install-recommends $debian_packages
RUN apt-get clean
# install provers
## CVC4 1.5
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.5-x86_64-linux-opt
RUN chmod a+x cvc4-1.5-x86_64-linux-opt
RUN cp cvc4-1.5-x86_64-linux-opt /usr/local/bin/cvc4-1.5
## CVC4 1.4
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt
RUN chmod a+x cvc4-1.4-x86_64-linux-opt
RUN cp cvc4-1.4-x86_64-linux-opt /usr/local/bin/cvc4-1.4
## Z3
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-debian-8.10.zip
RUN unzip z3-4.6.0-x64-debian-8.10.zip
RUN cp z3-4.6.0-x64-debian-8.10/bin/z3 /usr/local/bin/z3-4.6.0
# create user
RUN sudo adduser --disabled-password --gecos '' why3
USER why3
......
[uninstalled_prover coq85]
name = "Coq"
version = "8.5"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover coq86]
name = "Coq"
version = "8.6"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover coq861]
name = "Coq"
version = "8.6.1"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover coq872]
name = "Coq"
version = "8.7.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover Alt-Ergo1.01]
name = "Alt-Ergo"
version = "1.01"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover Alt-Ergo1.30]
name = "Alt-Ergo"
version = "1.30"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_95_2]
name = "Alt-Ergo"
version = "0.95.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_99_1]
name = "Alt-Ergo"
version = "0.99.1"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_1_01]
name = "Alt-Ergo"
version = "0.1.01"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_2_0_0]
name = "Alt-Ergo"
version = "2.0.0"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover cvc3_2_2]
name = "CVC3"
version = "2.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC3"
target_version = "2.4.1"
[uninstalled_prover cvc4_1_2]
name = "CVC4"
version = "1.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC4"
target_version = "1.4"
[uninstalled_prover cvc4_1_3]
name = "CVC4"
version = "1.3"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC4"
target_version = "1.4"
[uninstalled_prover Z33.2]
name = "Z3"
version = "3.2"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.3.2]
name = "Z3"
version = "4.3.2"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.4.0]
name = "Z3"
version = "4.4.0"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.4.1_noBV]
name = "Z3"
version = "4.4.1"
alternative = "noBV"
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = "noBV"
[uninstalled_prover Z34.4.1]
name = "Z3"
version = "4.4.1"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.5.0]
name = "Z3"
version = "4.5.0"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Eprover1.8-001]
name = "Eprover"
version = "1.8-001"
alternative = ""
policy = "remove"
[uninstalled_prover Eprover1.9.1-001]
name = "Eprover"
version = "1.9.1-001"
alternative = ""
policy = "remove"
[uninstalled_prover Eprover2.0]
name = "Eprover"
version = "2.0"
alternative = ""
policy = "remove"
[uninstalled_prover Gappa1.3.0]
name = "Gappa"
version = "1.3.0"
alternative = ""
policy = "remove"
[uninstalled_prover MetiTarski2.4]
name = "MetiTarski"
version = "2.4"
alternative = ""
policy = "remove"
[uninstalled_prover PolyPaver0.3]
name = "PolyPaver"
version = "0.3"
alternative = ""
policy = "remove"
[uninstalled_prover Vampire0.6]
name = "Vampire"
version = "0.6"
alternative = ""
policy = "remove"
[uninstalled_prover veriT201410]
name = "veriT"
version = "201410"
alternative = ""
policy = "remove"
......@@ -34,6 +34,13 @@ do
doc)
make doc
;;
nightly-bench-reduced)
bin/why3config --detect-provers
bench/ce-bench
sed -i why3.conf -e "s/running_provers_max = [0-9]*/running_provers_max = 1/"
cat misc/bench-few-provers-why3-conf >> why3.conf
examples/regtests.sh --reduced-mode
;;
esac
shift
done
......@@ -14,15 +14,17 @@ esac
GITBRANCH=`git rev-parse --abbrev-ref HEAD`
REPORTDIR=$PWD/../why3-reports-$GITBRANCH
if ! test -e "$REPORTDIR"; then
echo "directory '$REPORTDIR' for reports does not exist, aborting."
exit 2
fi
OUT=$REPORTDIR/nightly-bench.out
PREVIOUS=$REPORTDIR/nightly-bench.previous
DIFF=$REPORTDIR/nightly-bench.diff
REPORT=$REPORTDIR/nightly-bench.report
if ! test -e "$REPORTDIR"; then
echo "directory '$REPORTDIR' for reports does not exist, creating."
mkdir "$REPORTDIR"
touch "$PREVIOUS"
fi
DATE=`date --utc +%Y-%m-%d`
SUBJECT="Why3 [$GITBRANCH] bench : "
......@@ -84,45 +86,7 @@ perl -pi -e 's/running_provers_max = 2/running_provers_max = 4/' why3.conf
COQVER=$(bin/why3 --list-provers | sed -n -e 's/ Coq (\?\([0-9.]\+\).*/\1/p')
echo "Coq version detected: $COQVER" >> $REPORT
if test "$COQVER" != "" ; then
cat >> why3.conf <<EOF
[uninstalled_prover coq85]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.5"
[uninstalled_prover coq86]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.6"
[uninstalled_prover coq861]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.6.1"
[uninstalled_prover coq872]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.7.2"
EOF
sed bench-coq-why3-conf -e "s/@COQVER@/$COQVER/g" >> why3.conf
fi
# run the bench
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment