Commit ba088ef4 authored by Heiko Becker's avatar Heiko Becker

Make all scripts run evaluation 3 times

parent 232e3e49
......@@ -60,8 +60,22 @@ do
cd ..
#run coq checker
#run coq checker 3 times
echo "Working on Coq $CERTNAME" >>$2
RESULT=$( { /usr/bin/time -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 \
./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 \
./daisy/output/$CERTNAME.v; } 2>&1)
echo $RESULT >>$1
......
......@@ -57,13 +57,27 @@ do
cd ..
#run coq checker
#run coq checker 3 times
echo "Working on Coq $CERTNAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
#run HOL4 checker
rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -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 \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
#run HOL4 checker 3 times
cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" >>$2
......@@ -72,16 +86,48 @@ do
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=${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=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
cd ../../
# #run HOL4 binary
#run HOL4 binary 3 times
echo "Working on CakeML $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary
RESULT=$( { /usr/bin/time -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 \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary 3 times
echo "Working on Coq binary $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&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