diff --git a/Dockerfile b/Dockerfile
index d5b9f2a8150d85822c6378a27f23482f700e5c43..3e74ff5c875cff09e05e913041dd71cc8ab19201 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,4 +1,4 @@
-FROM ocaml/opam2:latest
+FROM debian:latest
 
 WORKDIR /root
 
@@ -10,13 +10,13 @@ RUN apt-get update && \
 
 # # Configure opam
 # RUN opam init --comp=4.05.0 --auto-setup && \
-RUN eval `opam config env`
+#RUN eval `opam config env`
 
-RUN cd /home/opam/opam-repository && git pull && cd
+#RUN cd /home/opam/opam-repository && git pull && cd
 
 # Install coq and dependencies
-RUN opam repo add coq-released https://coq.inria.fr/opam/released --set-default && \
-    opam update
+#RUN opam repo add coq-released https://coq.inria.fr/opam/released --set-default && \
+#    opam update
 
 ### Currently disabled because some lemmas are missing in 8.7.2
 ##Install coq 8.7.2 in a switch
@@ -26,11 +26,20 @@ RUN opam repo add coq-released https://coq.inria.fr/opam/released --set-default
 #RUN opam install coq.8.7.2 coq-flocq.2.6.1
 
 #Install coq 8.8 in a switch
-RUN opam switch create coq8.8 ocaml-base-compiler.4.05.0
-RUN opam install coq.8.8.2 coq-flocq.3.1.0
+#RUN opam switch create coq8.8 ocaml-base-compiler.4.05.0
+#RUN opam install coq.8.8.2 coq-flocq.3.1.0
 
 # Install polyml from git
 RUN git clone https://github.com/polyml/polyml.git polyml && \
     cd polyml && \
-    git checkout v5.7 && \
-    ./configure && make && make install
+    git checkout v5.8.2
+RUN cd polyml && ./configure --prefix=/usr && make && make install
+
+COPY ./hol4/.HOLCOMMIT HOLCOMMIT
+
+RUN git clone https://github.com/HOL-Theorem-Prover/HOL/ HOL && \
+    cd HOL && \
+    git checkout $(cat /root/HOLCOMMIT) && \
+    poly < tools/smart-configure.sml && \
+    bin/build
+RUN ln -s /root/HOL/bin/Holmake /usr/bin/Holmake
\ No newline at end of file
diff --git a/scripts/ci-hol4.sh b/scripts/ci-hol4.sh
index 384aadf96637e050e8d2ba4733e37194b19f8023..5923115aad3ecfbdc033679643f8362699b2b6bd 100755
--- a/scripts/ci-hol4.sh
+++ b/scripts/ci-hol4.sh
@@ -4,41 +4,41 @@
 HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
 FLOVERDIR="$(pwd)"
 
-#HOL4 always cloned exactly here --> must be in this folder
-if [ ! -d "./HOL4" ];
-then
-    echo "HOL4 not installed, starting to install HOL4 into current directory."
-    echo "If this is not intended, please abort with Ctrl-c"
-    sleep 5
-
-    git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
-    cd HOL4
-    git checkout $HOLCOMMIT
-    poly < tools/smart-configure.sml
-    bin/build
-    export HOLDIR="$(pwd)"
-    cd ../
-else
-    cd ./HOL4
-    export HOLDIR="$(pwd)"
-    git pull
-    CURRHOL="$(git rev-parse HEAD)"
-    if [[ "$CURRHOL" != "$HOLCOMMIT" ]];
-    then
-        echo "Updating HOL4 to latest version specified in .HOLCOMMIT"
-        git checkout $HOLCOMMIT
-        bin/build cleanAll
-        poly < tools/smart-configure.sml
-        bin/build
-    else
-        echo "HOL4 up-to-date"
-    fi
-    cd $FLOVERDIR
-fi
+##HOL4 always cloned exactly here --> must be in this folder
+#if [ ! -d "./HOL4" ];
+#then
+#    echo "HOL4 not installed, starting to install HOL4 into current directory."
+#    echo "If this is not intended, please abort with Ctrl-c"
+#    sleep 5
+#
+#    git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
+#    cd HOL4
+#    git checkout $HOLCOMMIT
+#    poly < tools/smart-configure.sml
+#    bin/build
+#    export HOLDIR="$(pwd)"
+#    cd ../
+#else
+#    cd ./HOL4
+#    export HOLDIR="$(pwd)"
+#    git pull
+#    CURRHOL="$(git rev-parse HEAD)"
+#    if [[ "$CURRHOL" != "$HOLCOMMIT" ]];
+#    then
+#        echo "Updating HOL4 to latest version specified in .HOLCOMMIT"
+#        git checkout $HOLCOMMIT
+#        bin/build cleanAll
+#        poly < tools/smart-configure.sml
+#        bin/build
+#    else
+#        echo "HOL4 up-to-date"
+#    fi
+#    cd $FLOVERDIR
+#fi
 
 cd ./hol4
 
-$HOLDIR/bin/Holmake
+Holmake
 
 #cd ./binary