Commit de675bb7 authored by Heiko Becker's avatar Heiko Becker

Update CakeML and Daisy to latest versions such that CI should be working now, update Dockerfile

parent 67d57ae8
......@@ -12,6 +12,10 @@ compile-coq:
only:
- master
script: ./scripts/ci-coq.sh
artifacts:
expire_in: 24h
paths:
- coq/
compile-hol:
stage: compile
......
FROM debian:latest
ENV HOLCOMMIT 60830f02ff6b86e0fd69ce6679614d497089b2eb
WORKDIR /root
#Necessary packages for opam
......@@ -26,6 +24,8 @@ RUN git clone https://github.com/polyml/polyml.git polyml && \
git checkout v5.7 && \
./configure && make && make install
ENV HOLCOMMIT 0de2c07679bd3773231f63059bbdd86050eeb452
# Download HOL4 and compile
RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
cd HOL4 && \
......
Subproject commit fc1b5c0d4bae293a50ff652a9c22ec68ea465d55
Subproject commit 87b9fec31854901afc0cb12a2255f17d0008a96f
Subproject commit 628362a23e7879d6db1eefd460acf16d49a83727
Subproject commit 120c3f18b89f91ef6697c1f29d2025cbe2369b9a
#!/bin/bash
eval `opam config env`
cd ./testcases/regression
#Coq regression tests
for fname in ./*.v; do
coqc -R ../../coq Flover $fname
if [ $? -eq 1 ]
if [ $? -eq 0 ]
then
echo "Successfully checked $fname"
else
echo "Checking $fname failed"
exit 1;
fi
echo "Successfully checked $fname"
done
#HOL4 regression tests
for fname in ./*.sml; do
FILEPRE=${fname/Script.sml/}
FILENAME=$FILEPRE
$HOLDIR/bin/Holmake ${fname/Script.sml/Theory.sig} -q
if [ $? -eq 1 ]
$HOLDIR/bin/Holmake ${fname/Script.sml/Theory.sig}
if [ $? -eq 0 ]
then
echo "Successfully checked $FILENAME"
else
echo "Checking $FILENAME has failed"
exit 1;
fi
echo "Successfully checked $FILENAME"
done
#Binary regression tests
for fname in ./*.txt; do
../../hol4/binary/cake_checker $fname
if [ $? -eq 1 ]
if [ $? -eq 0 ]
then
echo "Successfully checked $fname";
else
echo "Checking $fname has failed"
exit 1;
fi
echo "Successfully checked $fname";
done
COQAUX1 14eb2e5e017990f6a3f1ccef9be1fc57 /local/home/hbecker/Git_Repos/FloVer/testcases/regression/certificate_AdditionSimple.v
42 90 context_used ";"
91 123 context_used ";"
124 166 context_used ";"
167 194 context_used ";"
197 300 context_used ";"
301 424 context_used ";"
426 777 context_used ";"
933 939 VernacProof "tac:no using:no"
960 964 proof_build_time "0.013"
--- ErrorBound_additionSimple_Sound "0.013"
960 964 context_used ";"
960 964 proof_check_time "0.010"
--- vo_compile_time "0.759"
COQAUX1 7830f6aeda2c910507e270bf93518d00 /local/home/hbecker/Git_Repos/FloVer/testcases/regression/certificate_Doppler.v
42 90 context_used ";"
91 136 context_used ";"
137 169 context_used ";"
170 212 context_used ";"
213 255 context_used ";"
256 289 context_used ";"
290 332 context_used ";"
333 365 context_used ";"
366 412 context_used ";"
413 445 context_used ";"
446 488 context_used ";"
489 530 context_used ";"
531 572 context_used ";"
573 602 context_used ";"
603 652 context_used ";"
655 838 context_used ";"
839 1043 context_used ";"
1045 4798 context_used ";"
4935 4941 VernacProof "tac:no using:no"
4962 4966 proof_build_time "0.770"
--- ErrorBound_doppler_Sound "0.770"
4962 4966 context_used ";"
4962 4966 proof_check_time "0.719"
--- vo_compile_time "2.537"
COQAUX1 9cdd343852a339130dbc781256fbb137 /local/home/hbecker/Git_Repos/FloVer/testcases/regression/certificate_HimmilbeauLet.v
42 75 context_used ";"
76 119 context_used ";"
120 153 context_used ";"
154 196 context_used ";"
197 230 context_used ";"
231 274 context_used ";"
275 317 context_used ";"
318 351 context_used ";"
352 398 context_used ";"
399 441 context_used ";"
442 483 context_used ";"
484 530 context_used ";"
531 575 context_used ";"
576 620 context_used ";"
621 664 context_used ";"
665 694 context_used ";"
695 744 context_used ";"
745 810 context_used ";"
813 999 context_used ";"
1000 1156 context_used ";"
1158 5544 context_used ";"
5701 5707 VernacProof "tac:no using:no"
5728 5732 proof_build_time "0.228"
--- ErrorBound_himmilbeau_Sound "0.228"
5728 5732 context_used ";"
5728 5732 proof_check_time "0.229"
--- vo_compile_time "1.545"
......@@ -23,7 +23,7 @@ FloverMapTree_insert PlusC12u0 (( (1157)/(5), (2157)/(5)), (7771411516990528329)
val _ = store_thm ("ErrorBound_additionSimple_Sound",
``CertificateCheckerCmd RetPlusC12u0 absenv_additionSimple thePreconditionadditionSimple defVars_additionSimple``,
daisy_eval_tac \\ fs[REAL_INV_1OVER]);
flover_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
\ No newline at end of file
......@@ -34,7 +34,7 @@ FloverMapTree_insert (Var 5) (( (1567)/(5), (1807)/(5)) , (286015870425657721837
val _ = store_thm ("ErrorBound_doppler_Sound",
``CertificateCheckerCmd Lett15PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 absenv_doppler thePreconditiondoppler defVars_doppler``,
daisy_eval_tac \\ fs[REAL_INV_1OVER]);
flover_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
\ No newline at end of file
......@@ -37,7 +37,7 @@ FloverMapTree_insert (Var 4) (( (-30)/(1), (30)/(1)) , (803825900531996730762966
val _ = store_thm ("ErrorBound_himmilbeau_Sound",
``CertificateCheckerCmd Lett14PlusMultx10x10x21Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 absenv_himmilbeau thePreconditionhimmilbeau defVars_himmilbeau``,
daisy_eval_tac \\ fs[REAL_INV_1OVER]);
flover_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
\ No newline at end of file
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