Commit 06604887 authored by Joachim Bard's avatar Joachim Bard
Browse files

eval scripts: check with coq only once

parent 08889677
......@@ -62,6 +62,7 @@ do
--precision=Fixed32 \
--rangeMethod=smt \
--errorMethod=interval \
--subdiv \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
......@@ -78,19 +79,19 @@ do
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob
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=$( { $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=$( { $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=$( { $TIMECMD -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/
......
......@@ -94,18 +94,18 @@ do
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=$( { $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=$( { $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=$( { $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=$( { $TIMECMD -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/
......
......@@ -100,18 +100,18 @@ do
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=$( { $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=$( { $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=$( { $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=$( { $TIMECMD -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/
......
......@@ -100,18 +100,18 @@ do
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=$( { $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=$( { $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=$( { $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=$( { $TIMECMD -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/
......
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