Commit 99d68972 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'next' into new_ide

parents 2bf9572e 974eee74
......@@ -1714,6 +1714,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
bash bench/bench ".@OCAMLBEST@"
@echo ""
@if test "@enable_coq_tactic@" = "yes"; then \
echo "=== checking the Coq tactic ==="; \
$(MAKE) test-coq-tactic; fi
......
......@@ -87,7 +87,7 @@ invalid_goals () {
execute () {
pgm="bin/why3execute$suffix"
printf "$1 $2... "
printf " $1 $2... "
if $pgm $1 $2 > /dev/null 2>&1; then
echo "ok"
else
......@@ -103,7 +103,7 @@ extract_and_run () {
shift
prg=$1
shift
printf "$dir... "
printf " $dir... "
rm -f $dir/$prg
printf "clean... "
if BENCH=yes make -C $dir clean > /dev/null 2>&1; then
......@@ -150,7 +150,7 @@ extract_and_run () {
list_stuff () {
pgm="bin/why3$suffix"
printf '%s ' "$1"
printf ' %s ' "$1"
if $pgm $1 > /dev/null 2>&1; then
echo "ok"
else
......@@ -254,3 +254,6 @@ list_stuff --list-formats
list_stuff --list-metas
list_stuff --list-debug-flags
echo ""
echo "=== Checking realizations ==="
exec bench/check_realizations.sh
# cd to the directory of this script
cd `dirname $0`
#!/bin/bash
# temporary directory where we generate realizations
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
mkdir -p $TMPREAL/lib
res=0
echo "Testing isabelle realizations"
echo "Testing Isabelle realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/isabelle/ $TMPREAL/lib/
cp -r lib/isabelle $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/isabelle $TMPREAL/lib/isabelle`
if test "$TMPDIFF" = "" ; then
printf "Isabelle realizations OK\n"
else
printf "ISABELLE REALIZATIONS FAILED, please regenerate and prove them\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in $TMPREAL\n"
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
res=1
else
echo "Isabelle realizations OK"
fi
echo "Testing coq realizations"
echo "Testing Coq realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/coq/ $TMPREAL/lib/
cp -r lib/coq $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/coq $TMPREAL/lib/coq`
if test "$TMPDIFF" = "" ; then
printf "Coq realizations OK\n"
else
printf "COQ REALIZATIONS FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in $TMPREAL\n"
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
res=1
else
echo "Coq realizations OK"
fi
rm -r $TMPREAL
exit $res
......@@ -27,6 +27,3 @@ bin/why3config --detect-provers
# run the bench
make bench
# check that the realizations are ok
misc/check_realizations.sh
......@@ -137,9 +137,6 @@ else
echo "Counterexample regression tests succeeded. " >> $REPORT
fi
# check realizations
misc/check-realizations.sh >> $REPORT
# replay proofs
examples/regtests.sh &> $OUT
if test "$?" != "0" ; then
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment