misc/nightly-bench.sh

   1 #!/bin/bash
   2
   3
   4 case "$1" in
   5   "-mail")
   6         REPORTBYMAIL=$2;;
   7   "")
   8         REPORTBYMAIL=no;;
   9   *)
  10         echo "$0: Unknown option '$1'"
  11         exit 2
  12 esac
  13
  14 GITBRANCH=`git rev-parse --abbrev-ref HEAD`
  15 REPORTDIR=$PWD/../why3-reports-$GITBRANCH
  16
  17 OUT=$REPORTDIR/nightly-bench.out
  18 PREVIOUS=$REPORTDIR/nightly-bench.previous
  19 DIFF=$REPORTDIR/nightly-bench.diff
  20 REPORT=$REPORTDIR/nightly-bench.report
  21
  22 if ! test -e "$REPORTDIR"; then
  23     echo "directory '$REPORTDIR' for reports does not exist, creating."
  24     mkdir "$REPORTDIR"
  25     touch "$PREVIOUS"
  26 fi
  27
  28 LASTCOMMIT=$REPORTDIR/lastcommit
  29
  30 DATE=`date --utc +%Y-%m-%d`
  31 SUBJECT="Why3 [$GITBRANCH] bench : "
  32
  33 notify() {
  34     if test "$REPORTBYMAIL" == "no"; then
  35         cat $REPORT
  36     else
  37         mail -s "$SUBJECT" $REPORTBYMAIL < $REPORT
  38     fi
  39     exit 0
  40 }
  41
  42 LASTCOMMITHASH=$(cat $LASTCOMMIT 2>/dev/null || echo 'none')
  43 NEWCOMMITHASH=$(git rev-parse HEAD)
  44
  45 if test $LASTCOMMITHASH = $NEWCOMMITHASH; then
  46     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
  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
  53
  54 # configuration
  55 ./autogen.sh
  56 ./configure --enable-local &> $OUT
  57 if test "$?" != "0" ; then
  58     echo "Configure failed" >> $REPORT
  59     cat $OUT >> $REPORT
  60     SUBJECT="$SUBJECT configure failed"
  61     notify
  62 else
  63     echo "Configuration succeeded. " >> $REPORT
  64 fi
  65
  66 # compilation
  67 make -j4 &> $OUT
  68 if test "$?" != "0" ; then
  69     echo "Compilation failed" >> $REPORT
  70     tail -20 $OUT >> $REPORT
  71     SUBJECT="$SUBJECT compilation failed"
  72     notify
  73 else
  74     echo "Compilation succeeded. " >> $REPORT
  75 fi
  76
  77 # detection of provers
  78 bin/why3 config detect &> $OUT
  79 if test "$?" != "0" ; then
  80     echo "Prover detection failed" >> $REPORT
  81     cat $OUT >> $REPORT
  82     SUBJECT="$SUBJECT prover detection failed"
  83     notify
  84 else
  85     echo "Prover detection succeeded. " >> $REPORT
  86 fi
  87
  88 # increase number of cores used
  89 perl -pi -e 's/running_provers_max = 2/running_provers_max = 4/' why3.conf
  90
  91 # add uninstalled prover substitution policies
  92
  93 COQVER=$(bin/why3 config list-provers | sed -n -e 's/Coq (\?\([0-9.]\+\).*/\1/p')
  94 echo "Coq version detected: $COQVER" >> $REPORT
  95 if test "$COQVER" != "" ; then
  96   sed misc/bench-coq-why3-conf -e "s/@COQVER@/$COQVER/g" >> why3.conf
  97 fi
  98
  99 # run the bench
 100 make bench &> $OUT
 101 if test "$?" != "0" ; then
 102     echo "Make bench FAILED" >> $REPORT
 103     tail -20 $OUT >> $REPORT
 104     SUBJECT="$SUBJECT make bench failed,"
 105     # we do not notify yet, we try the examples also
 106     # notify
 107 else
 108     echo "Make bench succeeded. " >> $REPORT
 109 fi
 110
 111 # run regression bench for counterexamples
 112 bench/check-ce-bench &> $OUT
 113 if test "$?" != "0" ; then
 114     echo "Counterexample regression tests FAILED" >> $REPORT
 115     cat $OUT >> $REPORT
 116     SUBJECT="$SUBJECT (CE regression failed)"
 117 else
 118     echo "Counterexample regression tests succeeded. " >> $REPORT
 119 fi
 120
 121 # replay proofs
 122 examples/regtests.sh &> $OUT
 123 if test "$?" != "0" ; then
 124     SUBJECT="$SUBJECT failed"
 125     echo "Proof replay failed" >> $REPORT
 126 else
 127     SUBJECT="$SUBJECT successful"
 128     echo "REPLAY SUCCEEDED" >> $REPORT
 129 fi
 130
 131 # store the state for this day
 132 cp $OUT $REPORTDIR/regtests-$DATE
 133
 134 echo "Ending time (UTC): "`date --utc +%H:%M` >> $REPORT
 135
 136 # 3-line summary
 137 echo "" >> $REPORT
 138 tail -3 $OUT >> $REPORT
 139 echo "" >> $REPORT
 140
 141 # output the diff against previous run
 142 diff -u $PREVIOUS $OUT &> $DIFF
 143 if test "$?" == 0 ; then
 144     echo "---------- No difference with last bench ---------- " >> $REPORT
 145 else
 146     SUBJECT="$SUBJECT (with new differences)"
 147     if expr `cat $DIFF | wc -l` '>=' `cat $OUT | wc -l` ; then
 148         echo "------- Diff with last bench is larger than the bench itself ------" >> $REPORT
 149     else
 150         echo "--------------- Diff with last bench --------------" >> $REPORT
 151         echo "" >> $REPORT
 152         sed '1,2d' $DIFF >> $REPORT
 153     fi
 154     cp $OUT $PREVIOUS
 155 fi
 156
 157 # finally print the full state
 158 echo "" >> $REPORT
 159 echo "-------------- Full current state --------------" >> $REPORT
 160 echo "" >> $REPORT
 161 cat $OUT >> $REPORT
 162
 163 echo $NEWCOMMITHASH > $LASTCOMMIT
 164
 165 fi # end of test if LASTCOMMITHASH = NEWCOMMITHASH
 166
 167 # final notification after the replay
 168 notify