Commit ff37cc07 authored by Heiko Becker's avatar Heiko Becker

Fix Coq 8.7.2 compatobility

parent 3901659c
Require Import Flover.CertificateChecker Flover.floverParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Extraction Language OCaml.
Extraction Language Ocaml.
Extraction "./binary/CoqChecker.ml" runChecker.
\ No newline at end of file
#!/bin/bash
####################################################################################
# #
# Experiments for CPP 2018 Paper. Run daisy on all testcases in the "cpp2018" #
# directory. Then use the provers to get the runtimes and check the certificates #
# #
####################################################################################
PROVERS=(coq hol4 binary)
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
# FIXME: Use a proper directory or a parameter?
done < <(find $2 -name "*.scala" -print0)
DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_$DATE
echo "Creating HOL4 heap for evaluation"
cd ./hol4/output/
Holmake heap
cd ../../
for file in "${arr[@]}"
do
#Get the filename
FILEPATH=${file/daisy\//.\/}
FILE=${file/*\//}
FILENAME=${FILE/.scala/}
PMAP=${FILE/scala/txt}
CERTNAME="certificate_$FILENAME"
# Generate a certificate with Daisy
echo -n $FILENAME >>$1
cd ./daisy
if [ ! -f testcases/mixed-precision-maps/$PMAP ];
then
echo "Doing single precision eval for $FILENAME"
for prv in "${PROVERS[@]}"
do
/usr/bin/time -o $1 -a -f ", %e" ./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval
done
else
echo "Doing mixed-precision eval for $FILENAME"
for prv in "${PROVERS[@]}"
do
/usr/bin/time -o $1 -a -f ", %e" ./daisy $FILEPATH --certificate=$prv \
--errorMethod=interval \
--mixed-precision=testcases/mixed-precision-maps/$PMAP
done
fi
cd ..
#run coq checker
echo "Working on Coq $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" coqc -R ./coq Flover ./daisy/output/$CERTNAME.v
#run HOL4 checker
cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig"
/usr/bin/time -o $1 -a -f ", %e" Holmake $CERTNAME"Theory.sig"
cd ../../
# #run HOL4 binary
echo "Working on CakeML $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" hol4/binary/cake_checker ./daisy/output/$CERTNAME".txt"
# #run Coq binary
echo "Working on Coq binary $CERTNAME"
/usr/bin/time -o $1 -a -f ", %e" coq/binary/coq_checker_native ./daisy/output/$CERTNAME".txt"
mv ./daisy/output/certificate_* /tmp/artifact_$DATE/
#Add a linebreak
echo "">>$1
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