Commit 1c92efe7 authored by MARCHE Claude's avatar MARCHE Claude

night scripts

parent f9700415
#!/bin/bash
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
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
autoconf
./configure --enable-local 2>&1 > $OUT
if test "$?" != "0" ; then
echo "Configure failed" >> $REPORT
cat $OUT >> $REPORT
notify
else
echo "Configuration succeeded. " >> $REPORT
fi
# phase 3: compilation
make 2>&1 > $OUT
if test "$?" != "0" ; then
echo "Compilation failed" >> $REPORT
tail -20 $OUT >> $REPORT
notify
else
echo "Compilation succeeded. " >> $REPORT
fi
# do we want to do "make bench" ?
# phase 4: replay proofs
examples/regtests.sh 2>&1 > $OUT
if test "$?" != "0" ; then
echo "Proof replay failed" >> $REPORT
cat $OUT >> $REPORT
notify
else
echo "Replay succeeded. " >> $REPORT
fi
# final notification if everything is OK
notify
...@@ -4,15 +4,16 @@ ...@@ -4,15 +4,16 @@
cd `dirname $0` cd `dirname $0`
TMP=/tmp/why3regtests.out TMP=/tmp/why3regtests.out
res=0
run_dir () { run_dir () {
for f in `ls $1/*/why3session.xml`; do for f in `ls $1/*/why3session.xml`; do
d=`dirname $f` d=`dirname $f`
echo -n "Replaying "$d"... " echo -n "Replaying "$d"... "
if ! why3replayer $d 2>/dev/null > $TMP ; then if ! ../bin/why3replayer $d 2>/dev/null > $TMP ; then
echo "FAILED:" echo "FAILED:"
cat $TMP cat $TMP
# exit 1 res=1
else else
echo "OK" echo "OK"
fi fi
...@@ -27,4 +28,6 @@ echo "=== Programs ===" ...@@ -27,4 +28,6 @@ echo "=== Programs ==="
run_dir programs run_dir programs
echo "" echo ""
exit $res
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