nightly-bench.sh 3.94 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
38
automake --add-missing
MARCHE Claude's avatar
MARCHE Claude committed
39
./configure --enable-local &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
40
41
42
if test "$?" != "0" ; then
    echo "Configure failed" >> $REPORT
    cat $OUT >> $REPORT
43
    SUBJECT="$SUBJECT configure failed"
MARCHE Claude's avatar
MARCHE Claude committed
44
    notify
MARCHE Claude's avatar
MARCHE Claude committed
45
else
MARCHE Claude's avatar
MARCHE Claude committed
46
47
48
    echo "Configuration succeeded. " >> $REPORT
fi

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

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

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

74
# add uninstalled prover substitution policies
75
76
77

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

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

89
90
91
92
93
94
[uninstalled_prover policy1]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
95
target_version = "$COQVER"
96
97
98
99
100
101
102
103
104
version = "8.4pl4"

[uninstalled_prover policy2]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
105
106
version = "8.4pl5"

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

116
117
118
119
120
121
122
123
124
[uninstalled_prover policy4]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.5"

125
EOF
126
fi
127

MARCHE Claude's avatar
MARCHE Claude committed
128
129
130
131
132
133
134
135
136
137
138
# 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
139

MARCHE Claude's avatar
MARCHE Claude committed
140
141
# replay proofs
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
147
148
149
150
151
152
    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
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