Commit 6e4f45f1 authored by Joachim Bard's avatar Joachim Bard
Browse files

checking certificates 3 times again

parent dfc1cf2c
...@@ -78,19 +78,19 @@ do ...@@ -78,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