bench/check_realizations.sh

   1 #!/bin/bash
   2
   3 # temporary directory where we generate realizations
   4 TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
   5 mkdir -p $TMPREAL/lib
   6 res=0
   7
   8 echo "Testing Isabelle realizations"
   9 # We want to use the makefile to be sure to check exhaustively the
  10 # realizations that are built
  11 make GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
  12 LANG=C diff -u lib/isabelle/realizations $TMPREAL/lib/isabelle/realizations > $TMPREAL/diff-isabelle
  13 if test -s "$TMPREAL/diff-isabelle"; then
  14     echo "Isabelle realizations FAILED, please regenerate and prove them"
  15     cat $TMPREAL/diff-isabelle
  16     res=1
  17 else
  18     echo "Isabelle realizations OK"
  19 fi
  20
  21 echo "Testing Coq realizations"
  22 # First copy current realizations in a tmp directory
  23 cp -r lib/coq $TMPREAL/lib/
  24 # We want to use the makefile to be sure to check exhaustively the
  25 # realizations that are built
  26 make GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
  27 LANG=C diff -w -r -q -x '*.bak' -x '*~' -x '*.aux' lib/coq $TMPREAL/lib/coq > $TMPREAL/diff-coq
  28 if test -s "$TMPREAL/diff-coq"; then
  29     echo "Coq realizations FAILED, please regenerate and prove them"
  30     sed -e "s,$TMPREAL/lib/coq,new," $TMPREAL/diff-coq
  31     res=1
  32 else
  33     echo "Coq realizations OK"
  34 fi
  35
  36 rm -rf $TMPREAL
  37 exit $res