Merge branch 'affine_arithmetic' of https://gitlab.mpi-sws.org/AVA/FloVer into affine_arithmetic

scripts/eval_affine.sh

@@ -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

scripts/eval_fixed.sh

@@ -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)