Commit ef7c0b45 authored by Heiko Becker's avatar Heiko Becker

Remove timeout from evaluation since HOL4 Eval should terminate on all our examples

parent 9ad4f07f
......@@ -8,7 +8,6 @@
####################################################################################
#Configure a 40 minute stimeout for the HOL-Light scripts
TIMEOUT=40m
arr=()
while IFS= read -r -d $'\0'; do
......@@ -19,9 +18,9 @@ for file in "${arr[@]}"
do
echo $file
echo "Coq certificate"
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq >/dev/null
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq >/dev/null
echo "HOL Certificate"
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol4 >/dev/null
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol4 >/dev/null
echo ""
done
......@@ -39,7 +38,7 @@ for file in "${arrCoq[@]}"
do
echo $file
echo ""
/usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file
/usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file
done
cd ../hol4/output
......@@ -53,11 +52,5 @@ for file in "${arrHOL[@]}"
do
echo $file
echo ""
timeout $TIMEOUT /usr/bin/time -o $1 -a -f "%C %E" $HOLDIR/bin/Holmake ${file/Script.sml/Theory.sig}
RETVAL=$?
if [ $RETVAL -eq 124 ]
then echo "TIMEOUT "$file
else echo "SUCCESS "$file
fi
/usr/bin/time -o $1 -a -f "%C %E" $HOLDIR/bin/Holmake ${file/Script.sml/Theory.sig}
done
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