Commit 11427af6 authored by Michael Hanus's avatar Michael Hanus
Browse files

Test for "testing with verification" added

parent 6ca41157
......@@ -60,5 +60,6 @@ runtest:
cd currypp && $(MAKE) runtest
cd runcurry/Examples && ./test.sh
cd currycheck/Examples && ./test.sh
cd currycheck/Examples/WithVerification && ./test.sh
cd spicey/Examples && ./test.sh
cd xmldata/Examples && ./test.sh
#!/bin/sh
# Shell script to test the current set of examples
CURRYBIN="../../../../bin"
ALLTESTS="ListProp SortSpec"
VERBOSE=no
if [ "$1" = "-v" ] ; then
VERBOSE=yes
fi
# use the right Curry system for the tests:
PATH=$CURRYBIN:$PATH
export PATH
# clean up before
$CURRYBIN/cleancurry
# execute all tests:
CCOPTS=
LOGFILE=xxx$$
if [ $VERBOSE = yes ] ; then
$CURRYBIN/currycheck $CCOPTS $ALLTESTS
if [ $? -gt 0 ] ; then
exit 1
fi
else
$CURRYBIN/currycheck $CCOPTS $ALLTESTS > $LOGFILE 2>&1
if [ $? -gt 0 ] ; then
echo "ERROR in currycheck:"
cat $LOGFILE
exit 1
fi
fi
################ end of tests ####################
# Clean:
/bin/rm -f $LOGFILE *_PUBLIC.curry TEST*.curry
......@@ -29,8 +29,7 @@ AGDAIMPORTS="-i . -i /net/medoc/home/mh/home/languages_systems/agda/ial_org -i /
AGDAOPTS="--allow-unsolved-metas"
if [ -z "$AGDA" ] ; then
echo "WARNING: cannot check curry2verify ('agda' not found)"
exit
echo "WARNING: cannot completely test curry2verify ('agda' not found)"
fi
compile_to_agda()
......@@ -40,17 +39,21 @@ compile_to_agda()
CVOPTS=$2
if [ $VERBOSE = yes ] ; then
$CURRYBIN/curry2verify -t agda $CVOPTS $PROG
$AGDA $AGDAIMPORTS $AGDAOPTS TO-PROVE-*
if [ $? -gt 0 ] ; then
exit 1
if [ -x "$AGDA" ] ; then
$AGDA $AGDAIMPORTS $AGDAOPTS TO-PROVE-*
if [ $? -gt 0 ] ; then
exit 1
fi
fi
else
$CURRYBIN/curry2verify -t agda $CVOPTS $PROG >> $LOGFILE 2>&1
$AGDA $AGDAIMPORTS $AGDAOPTS TO-PROVE-* >> $LOGFILE 2>&1
if [ $? -gt 0 ] ; then
echo "ERROR in curry2verify:"
cat $LOGFILE
exit 1
if [ -x "$AGDA" ] ; then
$AGDA $AGDAIMPORTS $AGDAOPTS TO-PROVE-* >> $LOGFILE 2>&1
if [ $? -gt 0 ] ; then
echo "ERROR in curry2verify:"
cat $LOGFILE
exit 1
fi
fi
fi
/bin/rm -f TO-PROVE-*
......
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