Update Dockerfile to not depend on HOLCOMMIT variable in the file

Dockerfile

@@ -24,13 +24,22 @@ RUN git clone https://github.com/polyml/polyml.git polyml && \
     git checkout v5.7 && \
     ./configure && make && make install
 
-ENV HOLCOMMIT 0de2c07679bd3773231f63059bbdd86050eeb452
+ADD ./hol4/.HOLCOMMIT /root/HOLCOMMIT
+
+# RUN cat /root/HOLCOMMIT
+
+# RUN export HOLCOMMIT="$(cat /root/HOLCOMMIT)"
+
+# RUN echo $HOLCOMMIT
 
 # Download HOL4 and compile
 RUN git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4 && \
     cd HOL4 && \
-    git checkout $HOLCOMMIT &&\
+    git checkout `cat /root/HOLCOMMIT` &&\
+    git rev-parse HEAD &&\
     poly < tools/smart-configure.sml && \
     ./bin/build
 
+RUN echo "HOLDIR=/root/HOL4" >> /root/.profile
+
 ENV HOLDIR /root/HOL4

hol4/.HOLCOMMIT

+648910463f185d9e35f121dc9d47f1cf544be789

hol4/configure_hol.sh

+#!/bin/bash
+function display_help {
+    echo "configure_hol.sh - Check for environment variables and HOL4"
+    echo "                   commit hash to be correct"
+    echo ""
+    echo -e "--help\t Show this text"
+    echo -e " --init\t Initialize CakeML submodule to latest state"
+}
+
+INIT=no
+while [ $# != 0 ]; do
+   case "$1" in
+   --help)  display_help;;
+   --init) INIT=yes;;
+   *)
+   esac
+   shift
+ done
+
+if [[ "$HOLDIR" = "" ]];
+then
+    echo "ERROR: HOLDIR variable not set. Please configure the HOLDIR variable first"
+    exit 1
+fi
+
+DIR=pwd
+HOLCOMMIT="$(cat ./.HOLCOMMIT)"
+
+if [[ "$INIT" = "yes" ]];
+then
+    echo "Checking out CakeML submodule to correct state"
+    git submodule init
+    git submodule --update cakeml
+
+    echo "Checking out correct HOL4 version"
+    cd $HOLDIR
+    git checkout $HOLCOMMIT
+    $HOLDIR/bin/build cleanAll
+    poly < $HOLDIR/tools/smart-configure.sml
+    $HOLDIR/bin/build
+    cd $DIR
+else
+    cd $HOLDIR
+    CURR_HOL="$(git rev-parse HEAD)"
+
+    if [[ "$CURR_HOL" = "$HOLCOMMIT" ]]
+    then
+        echo "All set. HOL4 is on the correct commit."
+        exit 0
+    else
+        echo "Please make sure HOL4 uses the commit $HOLCOMMIT"
+        echo "or consider running the script with the --init parameter."
+    fi
+fi