Commit 1f194f2e authored by Joachim Bard's avatar Joachim Bard
Browse files

reverting eval_fixed script to old state

parent 6a7b9369
...@@ -62,7 +62,6 @@ do ...@@ -62,7 +62,6 @@ do
--precision=Fixed32 \ --precision=Fixed32 \
--rangeMethod=smt \ --rangeMethod=smt \
--errorMethod=interval \ --errorMethod=interval \
--subdiv \
--results-csv=$FILENAME.csv \ --results-csv=$FILENAME.csv \
>>$2 \ >>$2 \
; } 2>&1 ) ; } 2>&1 )
...@@ -79,19 +78,19 @@ do ...@@ -79,19 +78,19 @@ do
./daisy/output/$CERTNAME.v; } 2>&1) ./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1 echo -n $RESULT >>$1
# rm ./daisy/output/$CERTNAME.vo rm ./daisy/output/$CERTNAME.vo
# rm ./daisy/output/$CERTNAME.glob rm ./daisy/output/$CERTNAME.glob
#
# RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \ RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
# ./daisy/output/$CERTNAME.v; } 2>&1) ./daisy/output/$CERTNAME.v; } 2>&1)
# echo -n $RESULT >>$1 echo -n $RESULT >>$1
#
# rm ./daisy/output/$CERTNAME.vo rm ./daisy/output/$CERTNAME.vo
# rm ./daisy/output/$CERTNAME.glob rm ./daisy/output/$CERTNAME.glob
#
# RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \ RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
# ./daisy/output/$CERTNAME.v; } 2>&1) ./daisy/output/$CERTNAME.v; } 2>&1)
# echo -n $RESULT >>$1 echo -n $RESULT >>$1
# #run HOL4 checker 3 times # #run HOL4 checker 3 times
# cp ./daisy/output/*Script.sml ./hol4/output/ # 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