From 0cc503967bea5da97662cebe6c8f1e29810167ca Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Mon, 23 Apr 2018 16:02:14 +0200
Subject: [PATCH] Remove not useful stuff from dockerfile and start updating ci
 script for HOL4

---
 Dockerfile         | 20 --------------------
 scripts/ci-hol4.sh | 19 +++++++++++++++++++
 2 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 9b7f330..757f3cb 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -23,23 +23,3 @@ RUN git clone https://github.com/polyml/polyml.git polyml && \
     cd polyml && \
     git checkout v5.7 && \
     ./configure && make && make install
-
-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 `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
diff --git a/scripts/ci-hol4.sh b/scripts/ci-hol4.sh
index 366fc61..c1a449b 100755
--- a/scripts/ci-hol4.sh
+++ b/scripts/ci-hol4.sh
@@ -1,5 +1,24 @@
 #!/bin/sh
 
+if [[ $HOLDIR -eq "" ]]
+then
+    #We must be running on ci-server
+    echo "HOLDIR not set, starting to install HOL4 into ~/ for current user."
+    echo "If this is not intended, please abort with Ctrl-c"
+    sleep 5
+
+    #Set HOL4 commit variable
+    HOLCOMMIT="$(cat ./.HOLCOMMIT)"
+    pushd
+    cd ~/
+    git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
+    cd HOL4
+    git checkout $HOLCOMMIT
+    poly < tools/smart-configure.sml
+    bin/build
+    popd
+fi
+
 cd ./hol4
 #Run configure script to check the versions
 ./configure_hol.sh
-- 
GitLab