Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

nightly-bench.sh 4.42 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 15 16 17 18 19 20 21
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
22 23 24 25 26
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`
27
SUBJECT="Why3 [$GITBRANCH] bench : "
28

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


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

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

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

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

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

82
# add uninstalled prover substitution policies
83

Guillaume Melquiond's avatar
Guillaume Melquiond committed
84
COQVER=$(bin/why3 --list-provers | sed -n -e 's/  Coq (\?\([0-9.]\+\).*/\1/p')
85
echo "Coq version detected: $COQVER" >> $REPORT
86
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 117 118 119 120 121 122 123 124
[uninstalled_prover coq872]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.7.2"

125
EOF
126
fi
127

MARCHE Claude's avatar
MARCHE Claude committed
128 129 130 131
# run the bench
make bench &> $OUT
if test "$?" != "0" ; then
    echo "Make bench FAILED" >> $REPORT
132 133
    tail -20 $OUT >> $REPORT
    SUBJECT="$SUBJECT make bench failed,"
134 135
    # we do not notify yet, we try the examples also
    # notify
MARCHE Claude's avatar
MARCHE Claude committed
136 137 138 139
else
    echo "Make bench succeeded. " >> $REPORT
fi

140 141 142 143 144 145 146 147 148 149
# 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

MARCHE Claude's avatar
MARCHE Claude committed
150
# replay proofs
151
examples/regtests.sh &> $OUT
MARCHE Claude's avatar
MARCHE Claude committed
152
if test "$?" != "0" ; then
153
    SUBJECT="$SUBJECT failed"
MARCHE Claude's avatar
MARCHE Claude committed
154
    echo "Proof replay failed" >> $REPORT
MARCHE Claude's avatar
MARCHE Claude committed
155
else
156
    SUBJECT="$SUBJECT successful"
157
    echo "REPLAY SUCCEEDED" >> $REPORT
158 159 160 161 162
fi

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

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

165
# 3-line summary
166
echo "" >> $REPORT
167
tail -3 $OUT >> $REPORT
168 169
echo "" >> $REPORT

170 171 172 173 174
# output the diff against previous run
diff -u $PREVIOUS $OUT &> $DIFF
if test "$?" == 0 ; then
    echo "---------- No difference with last bench ---------- " >> $REPORT
else
175
    SUBJECT="$SUBJECT (with new differences)"
176 177 178 179 180 181 182
    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
183
    cp $OUT $PREVIOUS
MARCHE Claude's avatar
MARCHE Claude committed
184 185
fi

186 187 188 189 190 191 192
# 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
193
notify