Commit 7e36b027 authored by MARCHE Claude's avatar MARCHE Claude

night scripts for crontab

parent 1c92efe7
......@@ -4,23 +4,17 @@ OUT=/tmp/nightly-bench.out
REPORT=/tmp/nightly-bench.report
notify() {
# mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
cat $REPORT
mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
# cat $REPORT
exit 0
}
echo "== Why3 bench on `date` ==" > $REPORT
# phase 1: update the git repository
cd /tmp
# rm -rf why3
# git clone git://scm.gforge.inria.fr/why3/why3.git
# phase 2: configuration
cd why3
# configuration
autoconf
./configure --enable-local 2>&1 > $OUT
./configure --enable-local &> $OUT
if test "$?" != "0" ; then
echo "Configure failed" >> $REPORT
cat $OUT >> $REPORT
......@@ -29,8 +23,8 @@ else
echo "Configuration succeeded. " >> $REPORT
fi
# phase 3: compilation
make 2>&1 > $OUT
# compilation
make -j4 &> $OUT
if test "$?" != "0" ; then
echo "Compilation failed" >> $REPORT
tail -20 $OUT >> $REPORT
......@@ -39,10 +33,20 @@ else
echo "Compilation succeeded. " >> $REPORT
fi
# detection of provers
bin/why3config --detect-provers &> $OUT
if test "$?" != "0" ; then
echo "Prover detection failed" >> $REPORT
cat $OUT >> $REPORT
notify
else
echo "Prover detection succeeded. " >> $REPORT
fi
# do we want to do "make bench" ?
# phase 4: replay proofs
examples/regtests.sh 2>&1 > $OUT
# replay proofs
examples/regtests.sh &> $OUT
if test "$?" != "0" ; then
echo "Proof replay failed" >> $REPORT
cat $OUT >> $REPORT
......
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