Commit 0be38ed0 authored by Heiko Becker's avatar Heiko Becker

Minor script improvements

parent fc02e1b5
......@@ -44,7 +44,7 @@ cd coq
do
$FILEPRE = ${file/.v/}
$FILENAME=${FILEPRE/output/}
/usr/bin/time -o $1 -a -f "| $FILENAME | %e |" coqc -R ./ Daisy $file
/usr/bin/time -o $1 -a -f " $FILENAME , %e " coqc -R ./ Daisy $file
done
......@@ -63,7 +63,7 @@ for file in "${arrHOL[@]}"
do
$FILEPRE = ${file/Script.sml/}
$FILENAME=$FILEPRE
/usr/bin/time -o $1 -a -f "| $FILENAME | %e" Holmake ${file/Script.sml/Theory.sig}
/usr/bin/time -o $1 -a -f "$FILENAME , %e" Holmake ${file/Script.sml/Theory.sig}
done
# echo ""
......@@ -99,7 +99,7 @@ echo "################################################
do
$FILEPRE=${file/.txt/}
$FILENAME=$FILEPRE
/usr/bin/time -f "| $FILENAME | %e |" sh -c "../hol4/binary/cake_checker <$file"
/usr/bin/time -f " $FILENAME , %e " sh -c "../hol4/binary/cake_checker <$file"
echo $?
done
......@@ -112,6 +112,6 @@ echo "################################################"
do
$FILEPRE=${file/.txt/}
$FILENAME=$FILEPRE
/usr/bin/time -a -o $1 -f "| $FILENAME | %e |" sh -c "../coq/binary/coq_checker_native $file"
/usr/bin/time -a -o $1 -f " $FILENAME , %e " sh -c "../coq/binary/coq_checker_native $file"
echo $?
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