Start working on a CI for FloVer

.gitlab-ci.yml

@@ -12,7 +12,7 @@ stages:
   - compile
   - test
 
-compile:
+compile-daisy:
   stage: compile
   script: sbt clean compile
   artifacts:
@@ -21,6 +21,18 @@ compile:
         - target/
         - project/
 
+compile-coq:
+  stage: compile
+  script: cd coq && ./configure_coq.sh && make
+
+compile-hol:
+  stage: compile
+  script: cd hol4 && Holmake
+
+compile-binary:
+  stage: compile
+  script: cd hol4/binary && Holmake checkerBinaryTheory.uo && Holmake checker.S && Holmake cake_checker
+
 unit:
   stage: test
   dependencies:

Dockerfile

 FROM openjdk:8u141-jdk
 RUN touch /usr/lib/jvm/java-8-openjdk-amd64/release
 
+ENV HOLCOMMIT 60830f02ff6b86e0fd69ce6679614d497089b2eb
 ENV SBT_VERSION 0.13.15
 
 WORKDIR /root
@@ -14,13 +15,42 @@ RUN \
   apt-get install sbt && \
   sbt sbtVersion
 
-# Install mpfr
-RUN apt-get install libmpfr4
+# # Install mpfr
+# RUN apt-get install libmpfr4
 
-# Install Z3
-RUN apt-get install libgomp1 z3 
+# # Install Z3
+# RUN apt-get install libgomp1 z3
 
-# Install dReal
+# # Install dReal
+# RUN \
+#   curl -fsL https://github.com/dreal/dreal3/releases/download/v3.16.09.01/dReal-3.16.09.01-linux.tar.gz | tar xz && \
+#   ln -s ~/dReal-3.16.09.01-linux/bin/dReal /usr/bin/dReal
+
+# Install opam
 RUN \
-  curl -fsL https://github.com/dreal/dreal3/releases/download/v3.16.09.01/dReal-3.16.09.01-linux.tar.gz | tar xz && \
-  ln -s ~/dReal-3.16.09.01-linux/bin/dReal /usr/bin/dReal
+    wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
+
+# Configure opam
+RUN apt-get install -y build-essential aspcud m4 && \
+    opam init --comp=4.02.3 --auto-setup && \
+    eval `opam config env`
+
+# Install coq and dependencies
+RUN opam repo add coq-released https://coq.inria.fr/opam/released && \
+    opam update && \
+    opam install coq.8.7.2 coq-flocq
+
+# Install polyml from git
+RUN git clone https://github.com/polyml/polyml.git polyml && \
+    cd polyml && \
+    git checkout v5.7 && \
+    ./configure && make && make install
+
+# Download HOL4 and compile
+RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
+    cd HOL4 && \
+    git checkout $HOLCOMMIT &&\
+    poly < tools/smart-configure.sml && \
+    ./bin/build
+
+ENV HOLDIR /root/HOL4