nightly-bench.sh 3.59 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
#!/bin/bash

MARCHE Claude's avatar
MARCHE Claude committed
3 4 5

case "$1" in
  "-mail")
6
        REPORTBYMAIL=$2;;
MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10 11 12 13
  "")
        REPORTBYMAIL=no;;
  *)
        echo "$0: Unknown option '$1'"
        exit 2
esac

14
REPORTDIR=$PWD/../why3-reports
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17 18 19
OUT=$REPORTDIR/nightly-bench.out
PREVIOUS=$REPORTDIR/nightly-bench.previous
DIFF=$REPORTDIR/nightly-bench.diff
REPORT=$REPORTDIR/nightly-bench.report
DATE=`date --utc +%Y-%m-%d`
MARCHE Claude's avatar
MARCHE Claude committed
20

21 22
SUBJECT="Why3 nightly bench:"

MARCHE Claude's avatar
MARCHE Claude committed
23
notify() {
24
    if test "$REPORTBYMAIL" == "no"; then
MARCHE Claude's avatar
MARCHE Claude committed
25
        cat $REPORT
26 27
    else
        mail -s "$SUBJECT" $REPORTBYMAIL < $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
28
    fi
MARCHE Claude's avatar
MARCHE Claude committed
29 30 31 32
    exit 0
}


MARCHE Claude's avatar
MARCHE Claude committed
33
echo "== Why3 bench on $DATE ==" > $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
34
echo "Starting time (UTC): "`date --utc +%H:%M` >> $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
35

MARCHE Claude's avatar
MARCHE Claude committed
36
# configuration
MARCHE Claude's avatar
MARCHE Claude committed
37
autoconf
MARCHE Claude's avatar
MARCHE Claude committed
38
./configure --enable-local &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
39 40 41
if test "$?" != "0" ; then
    echo "Configure failed" >> $REPORT
    cat $OUT >> $REPORT
42
    SUBJECT="$SUBJECT configure failed"
MARCHE Claude's avatar
MARCHE Claude committed
43
    notify
MARCHE Claude's avatar
MARCHE Claude committed
44
else
MARCHE Claude's avatar
MARCHE Claude committed
45 46 47
    echo "Configuration succeeded. " >> $REPORT
fi

MARCHE Claude's avatar
MARCHE Claude committed
48 49
# compilation
make -j4 &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
50 51 52
if test "$?" != "0" ; then
    echo "Compilation failed" >> $REPORT
    tail -20 $OUT >> $REPORT
53
    SUBJECT="$SUBJECT compilation failed"
MARCHE Claude's avatar
MARCHE Claude committed
54
    notify
MARCHE Claude's avatar
MARCHE Claude committed
55
else
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58
    echo "Compilation succeeded. " >> $REPORT
fi

MARCHE Claude's avatar
MARCHE Claude committed
59 60 61 62 63
# detection of provers
bin/why3config --detect-provers &> $OUT
if test "$?" != "0" ; then
    echo "Prover detection failed" >> $REPORT
    cat $OUT >> $REPORT
64
    SUBJECT="$SUBJECT prover detection failed"
MARCHE Claude's avatar
MARCHE Claude committed
65
    notify
MARCHE Claude's avatar
MARCHE Claude committed
66
else
MARCHE Claude's avatar
MARCHE Claude committed
67 68 69
    echo "Prover detection succeeded. " >> $REPORT
fi

MARCHE Claude's avatar
MARCHE Claude committed
70
# increase number of cores used
71
perl -pi -e 's/running_provers_max = 2/running_provers_max = 4/' why3.conf
MARCHE Claude's avatar
MARCHE Claude committed
72

73
# add uninstalled prover substitution policies
74 75 76

COQVER=`bin/why3 --list-provers | sed -n -e 's/  Coq (\(.*\))/\1/p'`
if test "$COQVER" != "" ; then
77 78 79 80 81 82 83 84
cat >> why3.conf <<EOF

[uninstalled_prover policy0]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
85
target_version = "$COQVER"
86 87
version = "8.4pl4"

88 89 90 91 92 93
[uninstalled_prover policy1]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
94
target_version = "$COQVER"
95 96
version = "8.4pl5"

97 98 99 100 101 102
[uninstalled_prover policy2]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
103
target_version = "$COQVER"
104 105
version = "8.4pl2"

106
EOF
107
fi
108

MARCHE Claude's avatar
MARCHE Claude committed
109 110 111 112 113 114 115 116 117 118 119
# run the bench
make bench &> $OUT
if test "$?" != "0" ; then
    echo "Make bench FAILED" >> $REPORT
    cat $OUT >> $REPORT
    SUBJECT="$SUBJECT make bench failed"
    notify
else
    echo "Make bench succeeded. " >> $REPORT
fi

MARCHE Claude's avatar
MARCHE Claude committed
120

MARCHE Claude's avatar
MARCHE Claude committed
121 122
# replay proofs
examples/regtests.sh &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
123
if test "$?" != "0" ; then
124
    SUBJECT="$SUBJECT failed"
MARCHE Claude's avatar
MARCHE Claude committed
125
    echo "Proof replay failed" >> $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
126
else
127 128 129 130 131 132 133
    SUBJECT="$SUBJECT successful"
    echo " !!! REPLAY SUCCEEDED !!!  YAHOOOO !!! " >> $REPORT
fi

# store the state for this day
cp $OUT $REPORTDIR/regtests-$DATE

MARCHE Claude's avatar
MARCHE Claude committed
134 135
echo "Ending time (UTC): "`date --utc +%H:%M` >> $REPORT

136
# 3-line summary
137
echo "" >> $REPORT
138
tail -3 $OUT >> $REPORT
139 140
echo "" >> $REPORT

141 142 143 144 145
# output the diff against previous run
diff -u $PREVIOUS $OUT &> $DIFF
if test "$?" == 0 ; then
    echo "---------- No difference with last bench ---------- " >> $REPORT
else
146
    SUBJECT="$SUBJECT (with new differences)"
147 148 149 150 151 152 153
    if expr `cat $DIFF | wc -l` '>=' `cat $OUT | wc -l` ; then
        echo "------- Diff with last bench is larger than the bench itself ------" >> $REPORT
    else
        echo "--------------- Diff with last bench --------------" >> $REPORT
        echo "" >> $REPORT
        sed '1,2d' $DIFF >> $REPORT
    fi
154
    cp $OUT $PREVIOUS
MARCHE Claude's avatar
MARCHE Claude committed
155 156
fi

157 158 159 160 161 162 163
# finally print the full state
echo "" >> $REPORT
echo "-------------- Full current state --------------" >> $REPORT
echo "" >> $REPORT
cat $OUT >> $REPORT

# final notification after the replay
MARCHE Claude's avatar
MARCHE Claude committed
164
notify