Commit d7e3ebf6 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge

parent 29992b73
bytes: #bytes:
ocamlc -c CoqChecker.ml # ocamlc -c CoqChecker.ml
ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml # ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml
native: native:
ocamlc -c CoqChecker.ml ocamlc -c CoqChecker.ml
ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
all: bytes native all: native
INCLUDES = .. ../cakeml/compiler ../cakeml/compiler/backend INCLUDES = .. ../cakeml/compiler ../cakeml/compiler/backend ../cakeml/misc
OPTIONS = QUIT_ON_FAILURE OPTIONS = QUIT_ON_FAILURE
ifdef POLY ifdef POLY
......
Subproject commit 3f8f06e6f46b79db0217c67bc1842309900666b4 Subproject commit 9f7a2e8b53e4f091ae49340aed425376ed30ae26
...@@ -24,7 +24,7 @@ do ...@@ -24,7 +24,7 @@ do
FILENAME=${FILEPRE/.\/testcases\/cpp2018\//} FILENAME=${FILEPRE/.\/testcases\/cpp2018\//}
PMAPSUFF=${file/scala/txt} PMAPSUFF=${file/scala/txt}
PMAP=${PMAPSUFF/.\/testcases\/cpp2018\//} PMAP=${PMAPSUFF/.\/testcases\/cpp2018\//}
/usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=coq --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/$PMAP # /usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=coq --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/$PMAP
#echo "HOL4 Certificate" #echo "HOL4 Certificate"
/usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=hol4 --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/$PMAP /usr/bin/time -o $1 -a -f " $FILENAME , %e " ./daisy $file --certificate=hol4 --errorMethod=interval --mixed-precision=testcases/mixed-precision-maps/$PMAP
#echo "HOL4 Binary Certificate" #echo "HOL4 Binary Certificate"
...@@ -33,8 +33,8 @@ do ...@@ -33,8 +33,8 @@ do
done done
echo "################################################ echo "################################################
Certificate test - Coq Certificate test - Coq
################################################" >>$1 ###############################################" >>$1
cd coq cd coq
arrCoq=() arrCoq=()
......
...@@ -781,7 +781,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -781,7 +781,7 @@ object CertificatePhase extends DaisyPhase {
"Proof.\n vm_compute; auto.\nQed.\n" "Proof.\n vm_compute; auto.\nQed.\n"
} else if (prover == "hol4"){ } else if (prover == "hol4"){
"val _ = store_thm (\""+s"ErrorBound_${fName}_Sound"+"\",\n" + "val _ = store_thm (\""+s"ErrorBound_${fName}_Sound"+"\",\n" +
s"``CertificateCheckerCmd $lastGenName $analysisResultName $precondName $defVarsName``,\n daisy_eval_tac \\ fs[]);\n" s"``CertificateCheckerCmd $lastGenName $analysisResultName $precondName $defVarsName``,\n daisy_eval_tac \\\\ fs[]);\n"
} else } else
"" ""
......
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