Commit a1f9305b authored by Heiko Becker's avatar Heiko Becker

Fix another bug in evaluation script

parent 7a1a65a0
......@@ -83,7 +83,8 @@ do
cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" >>$2
RESULT=$( { /usr/bin/time -f ", %e" Holmake $CERTNAME"Theory.sig" >>$2; } 2>&1)
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${${RESULT#M1}%%M2}
echo -n $RESULT >>$1
cd ../../
......@@ -91,13 +92,13 @@ do
# #run HOL4 binary
echo "Working on CakeML $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/$CERTNAME".txt" >>$2; } 2>&1)
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary
echo "Working on Coq binary $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/$CERTNAME".txt" >>$2; } 2>&1)
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo $RESULT >>$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