nightly-bench.sh 4.24 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
GITBRANCH=`git rev-parse --abbrev-ref HEAD`
REPORTDIR=$PWD/../why3-reports-$GITBRANCH

MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20
OUT=$REPORTDIR/nightly-bench.out
PREVIOUS=$REPORTDIR/nightly-bench.previous
DIFF=$REPORTDIR/nightly-bench.diff
REPORT=$REPORTDIR/nightly-bench.report
21 22 23 24 25 26 27

if ! test -e "$REPORTDIR"; then
    echo "directory '$REPORTDIR' for reports does not exist, creating."
    mkdir "$REPORTDIR"
    touch "$PREVIOUS"
fi

28 29
LASTCOMMIT=$REPORTDIR/lastcommit

MARCHE Claude's avatar
MARCHE Claude committed
30
DATE=`date --utc +%Y-%m-%d`
31
SUBJECT="Why3 [$GITBRANCH] bench : "
32

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

42 43
LASTCOMMITHASH=$(cat $LASTCOMMIT 2>/dev/null || echo 'none')
NEWCOMMITHASH=$(git rev-parse HEAD)
MARCHE Claude's avatar
MARCHE Claude committed
44

45 46
if test $LASTCOMMITHASH = $NEWCOMMITHASH; then
    echo "Not running nightly bench: last commit is the same as for previous run" > $REPORT
47
    SUBJECT="$SUBJECT not run (no new commit)"
48
else
MARCHE Claude's avatar
MARCHE Claude committed
49
echo "== Why3 bench on $DATE ==" > $REPORT
50
echo "Starting time (UTC): "`date --utc +%H:%M` >> $REPORT
51
echo "Current branch: "$GITBRANCH >> $REPORT
52
echo "Current commit: "$NEWCOMMITHASH >> $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
53

54
# configuration
MARCHE Claude's avatar
MARCHE Claude committed
55
autoconf
56
automake --add-missing
57
./configure --enable-local &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
58 59 60
if test "$?" != "0" ; then
    echo "Configure failed" >> $REPORT
    cat $OUT >> $REPORT
61
    SUBJECT="$SUBJECT configure failed"
MARCHE Claude's avatar
MARCHE Claude committed
62
    notify
MARCHE Claude's avatar
MARCHE Claude committed
63
else
MARCHE Claude's avatar
MARCHE Claude committed
64 65 66
    echo "Configuration succeeded. " >> $REPORT
fi

67 68
# compilation
make -j4 &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71
if test "$?" != "0" ; then
    echo "Compilation failed" >> $REPORT
    tail -20 $OUT >> $REPORT
72
    SUBJECT="$SUBJECT compilation failed"
MARCHE Claude's avatar
MARCHE Claude committed
73
    notify
MARCHE Claude's avatar
MARCHE Claude committed
74
else
MARCHE Claude's avatar
MARCHE Claude committed
75 76 77
    echo "Compilation succeeded. " >> $REPORT
fi

78 79 80 81 82
# detection of provers
bin/why3config --detect-provers &> $OUT
if test "$?" != "0" ; then
    echo "Prover detection failed" >> $REPORT
    cat $OUT >> $REPORT
83
    SUBJECT="$SUBJECT prover detection failed"
84
    notify
MARCHE Claude's avatar
MARCHE Claude committed
85
else
86 87 88
    echo "Prover detection succeeded. " >> $REPORT
fi

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

92
# add uninstalled prover substitution policies
93

94
COQVER=$(bin/why3 --list-provers | sed -n -e 's/  Coq (\?\([0-9.]\+\).*/\1/p')
95
echo "Coq version detected: $COQVER" >> $REPORT
96
if test "$COQVER" != "" ; then
97
sed bench-coq-why3-conf -e "s/@COQVER@/$COQVER/g"  >> why3.conf
98
fi
99

100 101 102 103
# run the bench
make bench &> $OUT
if test "$?" != "0" ; then
    echo "Make bench FAILED" >> $REPORT
104 105
    tail -20 $OUT >> $REPORT
    SUBJECT="$SUBJECT make bench failed,"
106 107
    # we do not notify yet, we try the examples also
    # notify
108 109 110 111
else
    echo "Make bench succeeded. " >> $REPORT
fi

112 113 114 115 116 117 118 119 120 121
# 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

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

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

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

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

142 143 144 145 146
# output the diff against previous run
diff -u $PREVIOUS $OUT &> $DIFF
if test "$?" == 0 ; then
    echo "---------- No difference with last bench ---------- " >> $REPORT
else
147
    SUBJECT="$SUBJECT (with new differences)"
148 149 150 151 152 153 154
    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
155
    cp $OUT $PREVIOUS
MARCHE Claude's avatar
MARCHE Claude committed
156 157
fi

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

164 165 166 167
echo $NEWCOMMITHASH > $LASTCOMMIT

fi # end of test if LASTCOMMITHASH = NEWCOMMITHASH

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