check_realizations.sh 1.25 KB
Newer Older
1
#!/bin/bash
2 3 4 5

# temporary directory where we generate realizations
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
mkdir -p $TMPREAL/lib
6
res=0
7

8
echo "Testing Isabelle realizations"
9 10
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
11
make GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
12
LANG=C diff lib/isabelle $TMPREAL/lib/isabelle/realizations.* > $TMPREAL/diff-isabelle
13 14
if test -s "$TMPREAL/diff-isabelle"; then
    echo "Isabelle realizations FAILED, please regenerate and prove them"
15
    cat $TMPREAL/diff-isabelle
16
    res=1
17 18
else
    echo "Isabelle realizations OK"
19 20
fi

21
echo "Testing Coq realizations"
22
# First copy current realizations in a tmp directory
23
cp -r lib/coq $TMPREAL/lib/
24 25
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
26 27 28 29 30
make GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
LANG=C diff -r -q -x '*.bak' -x '*~' -x '*.aux' lib/coq $TMPREAL/lib/coq > $TMPREAL/diff-coq
if test -s "$TMPREAL/diff-coq"; then
    echo "Coq realizations FAILED, please regenerate and prove them"
    sed -e "s,$TMPREAL/lib/coq,new," $TMPREAL/diff-coq
31
    res=1
32 33
else
    echo "Coq realizations OK"
34
fi
35 36 37

rm -r $TMPREAL
exit $res