check_realizations.sh 1.39 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
# First copy current realizations in a tmp directory
10
cp -r lib/isabelle $TMPREAL/lib/
11 12
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
13 14 15 16 17
make GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
LANG=C diff -r -q -x '*.bak' -x '*~' -x '*.aux' lib/isabelle $TMPREAL/lib/isabelle > $TMPREAL/diff-isabelle
if test -s "$TMPREAL/diff-isabelle"; then
    echo "Isabelle realizations FAILED, please regenerate and prove them"
    sed -e "s,$TMPREAL/lib/isabelle,new," $TMPREAL/diff-isabelle
18
    res=1
19 20
else
    echo "Isabelle realizations OK"
21 22
fi

23
echo "Testing Coq realizations"
24
# First copy current realizations in a tmp directory
25
cp -r lib/coq $TMPREAL/lib/
26 27
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
28 29 30 31 32
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
33
    res=1
34 35
else
    echo "Coq realizations OK"
36
fi
37 38 39

rm -r $TMPREAL
exit $res