Commit a3663215 authored by Heiko Becker's avatar Heiko Becker

Tweak eval script to make log more accurate

parent 8cd47ba2
...@@ -13,15 +13,15 @@ arr=() ...@@ -13,15 +13,15 @@ arr=()
while IFS= read -r -d $'\0'; do while IFS= read -r -d $'\0'; do
arr+=("$REPLY") arr+=("$REPLY")
# FIXME: Use a proper directory or a parameter? # FIXME: Use a proper directory or a parameter?
done < <(find $2 -name "*.scala" -print0) done < <(find $3 -name "*.scala" -print0)
DATE=`date +%H%M%d%m%y` DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_$DATE mkdir /tmp/artifact_$DATE
echo "Creating HOL4 heap for evaluation" echo "Creating HOL4 heap for evaluation" >>$2
cd ./hol4/output/ cd ./hol4/output/
Holmake heap Holmake heap >>$2
cd ../../ cd ../../
for file in "${arr[@]}" for file in "${arr[@]}"
...@@ -37,47 +37,64 @@ do ...@@ -37,47 +37,64 @@ do
cd ./daisy cd ./daisy
if [ ! -f testcases/mixed-precision-maps/$PMAP ]; if [ ! -f testcases/mixed-precision-maps/$PMAP ];
then then
echo "Doing single precision eval for $FILENAME" echo "Doing single precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}" for prv in "${PROVERS[@]}"
do do
/usr/bin/time -o $1 -a -f ", %e" ./daisy $FILEPATH --certificate=$prv \ RESULT=$( { /usr/bin/time -f ", %e" \
--errorMethod=interval ./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval \
--results-csv=$FILENAME \
>>$2 \
; } 2>&1 )
echo -n $RESULT >> $1
done done
else else
echo "Doing mixed-precision eval for $FILENAME" echo "Doing mixed-precision eval for $FILENAME" >>$2
for prv in "${PROVERS[@]}" for prv in "${PROVERS[@]}"
do do
/usr/bin/time -o $1 -a -f ", %e" ./daisy $FILEPATH --certificate=$prv \ RESULT=$( { /usr/bin/time -f ", %e" \
--errorMethod=interval \ ./daisy $FILEPATH --certificate=$prv \
--mixed-precision=testcases/mixed-precision-maps/$PMAP --errorMethod=interval \
--mixed-precision=testcases/mixed-precision-maps/$PMAP \
--results-csv=$FILENAME \
>>$2 \
; } 2>&1)
echo -n $RESULT >> $1
done done
fi fi
mv ./output/$FILENAME.csv /tmp/artifact_$DATE
cd .. cd ..
#run coq checker #run coq checker
echo "Working on Coq $CERTNAME" echo "Working on Coq $CERTNAME" >>$2
/usr/bin/time -o $1 -a -f ", %e" coqc -R ./coq Flover ./daisy/output/$CERTNAME.v RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
#run HOL4 checker #run HOL4 checker
cp ./daisy/output/*Script.sml ./hol4/output/ cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/ cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" echo "Working on $CERTNAME Theory.sig" >>$2
/usr/bin/time -o $1 -a -f ", %e" Holmake $CERTNAME"Theory.sig" RESULT=$( { /usr/bin/time -f ", %e" Holmake $CERTNAME"Theory.sig" >>$2; } 2>&1)
echo -n $RESULT >>$1
cd ../../ cd ../../
# #run HOL4 binary # #run HOL4 binary
echo "Working on CakeML $CERTNAME" echo "Working on CakeML $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" hol4/binary/cake_checker ./daisy/output/$CERTNAME".txt" RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/$CERTNAME".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary # #run Coq binary
echo "Working on Coq binary $CERTNAME" echo "Working on Coq binary $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" coq/binary/coq_checker_native ./daisy/output/$CERTNAME".txt" RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/$CERTNAME".txt" >>$2; } 2>&1)
mv ./daisy/output/certificate_* /tmp/artifact_$DATE/ echo $RESULT >>$1
#Add a linebreak mv ./daisy/output/certificate_* /tmp/artifact_$DATE/
echo "">>$1
done done
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