Commit 7cabfaa8 authored by Heiko Becker's avatar Heiko Becker

Make eval_interval platform independent

parent 6387e298
......@@ -11,6 +11,16 @@
# #
##############################################################################
TIMECMD=""
unameOut="$(uname -s)"
case "${unameOut}" in
Linux*) TIMECMD=/usr/bin/time;;
Darwin*) machine=/usr/local/bin/time;;
# CYGWIN*) machine=Cygwin;;
# MINGW*) machine=MinGw;;
# *) machine="UNKNOWN:${unameOut}"
esac
PROVERS=(coq hol4 binary)
......@@ -48,7 +58,7 @@ do
echo "Doing single precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}"
do
RESULT=$( { /usr/bin/time -f ", %e" \
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval \
--results-csv=$FILENAME.csv \
......@@ -60,7 +70,7 @@ do
echo "Doing mixed-precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}"
do
RESULT=$( { /usr/bin/time -f ", %e" \
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval \
--mixed-precision=testcases/daisy-mixed-precision-maps/$PMAP \
......@@ -77,19 +87,19 @@ do
#run coq checker 3 times
echo "Working on Coq $CERTNAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
......@@ -97,21 +107,21 @@ do
cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" >>$2
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
rm ./certificate_*Theory*
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
rm ./certificate_*Theory*
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
......@@ -121,31 +131,31 @@ do
#run HOL4 binary 3 times
echo "Working on CakeML $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary
echo "Working on Coq binary $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo $RESULT >>$1
......
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