nightly-bench.sh 4.15 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=`bin/why3 --list-provers | sed -n -e 's/  Coq (\(.*\))/\1/p'`
if test "$COQVER" != "" ; then
87 88
cat >> why3.conf <<EOF

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

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

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

116
EOF
117
fi
118

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

130 131 132 133 134 135 136 137 138 139
# 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

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

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

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

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

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

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