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

3 4 5

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

14 15 16 17 18 19 20 21 22

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

MARCHE Claude's avatar
MARCHE Claude committed
23 24 25 26 27
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`
28
SUBJECT="Why3 [$GITBRANCH] bench : "
29

MARCHE Claude's avatar
MARCHE Claude committed
30
notify() {
31
    if test "$REPORTBYMAIL" == "no"; then
32
        cat $REPORT
33 34
    else
        mail -s "$SUBJECT" $REPORTBYMAIL < $REPORT
35
    fi
MARCHE Claude's avatar
MARCHE Claude committed
36 37 38 39
    exit 0
}


MARCHE Claude's avatar
MARCHE Claude committed
40
echo "== Why3 bench on $DATE ==" > $REPORT
41
echo "Starting time (UTC): "`date --utc +%H:%M` >> $REPORT
42 43
echo "Current branch: "$GITBRANCH >> $REPORT
echo "Current commit: "`git rev-parse HEAD` >> $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
44

45
# configuration
MARCHE Claude's avatar
MARCHE Claude committed
46
autoconf
47
automake --add-missing
48
./configure --enable-local &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
49 50 51
if test "$?" != "0" ; then
    echo "Configure failed" >> $REPORT
    cat $OUT >> $REPORT
52
    SUBJECT="$SUBJECT configure failed"
MARCHE Claude's avatar
MARCHE Claude committed
53
    notify
MARCHE Claude's avatar
MARCHE Claude committed
54
else
MARCHE Claude's avatar
MARCHE Claude committed
55 56 57
    echo "Configuration succeeded. " >> $REPORT
fi

58 59
# compilation
make -j4 &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
60 61 62
if test "$?" != "0" ; then
    echo "Compilation failed" >> $REPORT
    tail -20 $OUT >> $REPORT
63
    SUBJECT="$SUBJECT compilation failed"
MARCHE Claude's avatar
MARCHE Claude committed
64
    notify
MARCHE Claude's avatar
MARCHE Claude committed
65
else
MARCHE Claude's avatar
MARCHE Claude committed
66 67 68
    echo "Compilation succeeded. " >> $REPORT
fi

69 70 71 72 73
# detection of provers
bin/why3config --detect-provers &> $OUT
if test "$?" != "0" ; then
    echo "Prover detection failed" >> $REPORT
    cat $OUT >> $REPORT
74
    SUBJECT="$SUBJECT prover detection failed"
75
    notify
MARCHE Claude's avatar
MARCHE Claude committed
76
else
77 78 79
    echo "Prover detection succeeded. " >> $REPORT
fi

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

83
# add uninstalled prover substitution policies
84

85 86
COQVER=$(why3 --list-provers | sed -n -e 's/  Coq (\?\([0-9.]\+\).*/\1/p')
echo "Coq version detected: $COQVER" >> $REPORT
87
if test "$COQVER" != "" ; then
88 89
cat >> why3.conf <<EOF

90
[uninstalled_prover coq85]
91 92 93 94 95
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
96
target_version = "$COQVER"
97
version = "8.5"
98

99
[uninstalled_prover coq86]
100 101 102 103 104 105
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
106
version = "8.6"
107

108 109 110 111 112 113 114 115 116
[uninstalled_prover coq861]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.6.1"

117
EOF
118
fi
119

120 121 122 123 124 125 126 127 128 129 130
# 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

131 132 133 134 135 136 137 138 139 140
# run regression bench for counterexamples
bench/ce-bench &> $OUT
if test "$?" != "0" ; then
    echo "Counterexample regression tests FAILED" >> $REPORT
    cat $OUT >> $REPORT
    SUBJECT="$SUBJECT (CE regression failed)"
else
    echo "Counterexample regression tests succeeded. " >> $REPORT
fi

141
# replay proofs
142
examples/regtests.sh &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
143
if test "$?" != "0" ; then
144
    SUBJECT="$SUBJECT failed"
MARCHE Claude's avatar
MARCHE Claude committed
145
    echo "Proof replay failed" >> $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
146
else
147
    SUBJECT="$SUBJECT successful"
148
    echo "REPLAY SUCCEEDED" >> $REPORT
149 150 151 152 153
fi

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

154 155
echo "Ending time (UTC): "`date --utc +%H:%M` >> $REPORT

156
# 3-line summary
157
echo "" >> $REPORT
158
tail -3 $OUT >> $REPORT
159 160
echo "" >> $REPORT

161 162 163 164 165
# output the diff against previous run
diff -u $PREVIOUS $OUT &> $DIFF
if test "$?" == 0 ; then
    echo "---------- No difference with last bench ---------- " >> $REPORT
else
166
    SUBJECT="$SUBJECT (with new differences)"
167 168 169 170 171 172 173
    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
174
    cp $OUT $PREVIOUS
MARCHE Claude's avatar
MARCHE Claude committed
175 176
fi

177 178 179 180 181 182 183
# 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
184
notify