Added OpenTheory into base docker image

narsis77 · Jan 3, 2023 · ebb5193 · ebb5193
1 parent 270b8c6
commit ebb5193
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 10 deletions.
diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
@@ -7,15 +7,16 @@
 FROM binghelisp/hol-dev:latest
 
 # Hardware specification for Windows and Linux virtual machines: 2-core CPU (x86_64)
-ARG BUILD_OPT="--expk -j2"
+ARG BUILD_OPT="--expk -j4"
+ARG ML_PROG=poly
 
 WORKDIR /ML/HOL
 
 # copy all files to the docker image
 COPY --link . .
 
 # build HOL
-RUN poly < tools/smart-configure.sml 
+RUN ${ML_PROG} < tools/smart-configure.sml 
 RUN bin/build ${BUILD_OPT}
 
 ENV PATH=/ML/HOL/bin:$PATH

diff --git a/developers/docker-ci/base/.emacs b/developers/docker-ci/base/.emacs
@@ -4,4 +4,4 @@
 
 (setq hol-executable     "/ML/HOL/bin/hol")
 (setq holmake-executable "/ML/HOL/bin/Holmake")
-(setq indent-tabs-mode   nil)
+(setq indent-tabs-mode nil)
diff --git a/developers/docker-ci/base/Dockerfile b/developers/docker-ci/base/Dockerfile
@@ -8,6 +8,7 @@
 FROM debian:stable
 
 WORKDIR /ML
+VOLUME /ML
 
 # Use this mode when you need zero interaction while installing or upgrading the system via apt
 ENV DEBIAN_FRONTEND=noninteractive
@@ -17,15 +18,15 @@ ENV LD_LIBRARY_PATH=/usr/local/lib
 RUN apt-get update -qy
 RUN apt-get install -qy build-essential graphviz git libgmp-dev curl wget
 
-# optional packages
+# optional packages (IDE)
 RUN apt-get install -qy emacs-nox vim automake
 RUN apt-get clean
 
-# install Mlton (https://github.com/MLton/mlton.git)
-RUN wget -q https://github.com/MLton/mlton/releases/download/on-20201002-release/mlton-20201002-1.amd64-linux.tgz
-RUN tar xzf mlton-20201002-1.amd64-linux.tgz
-RUN make -C mlton-20201002-1.amd64-linux
-RUN rm -rf mlton-20201002-1.amd64-linux*
+# install MLton (https://github.com/MLton/mlton.git)
+RUN wget -q https://github.com/MLton/mlton/releases/download/on-20210117-release/mlton-20210117-1.amd64-linux-glibc2.31.tgz
+RUN tar xzf mlton-20210117-1.amd64-linux-glibc2.31.tgz
+RUN make -C mlton-20210117-1.amd64-linux-glibc2.31
+RUN rm -rf mlton-20210117-1.amd64-linux-glibc2.31*
 
 # install polyml (https://github.com/polyml/polyml.git)
 RUN wget -q -O polyml-5.9.tar.gz https://github.com/polyml/polyml/archive/refs/tags/v5.9.tar.gz
@@ -40,9 +41,18 @@ RUN tar xzf mosml-ver-2.10.1.tar.gz
 RUN make -C mosml-ver-2.10.1/src world
 RUN make -C mosml-ver-2.10.1/src install
 
+# install OpenTheory
+RUN wget -q -O /root/opentheory-local.tar.gz https://github.com/binghe/opentheory/releases/download/v1.5/opentheory-local.tar.gz
+RUN cd /root && tar xzf opentheory-local.tar.gz
+RUN wget -q -O opentheory-1.5.tar.gz https://github.com/binghe/opentheory/archive/refs/tags/v1.5.tar.gz
+RUN tar xzf opentheory-1.5.tar.gz
+RUN make -C opentheory-1.5 mlton
+RUN cp opentheory-1.5/bin/mlton/opentheory /usr/local/bin
+
 # for Emacs
-COPY .emacs /root/
+COPY .emacs /root
 
 # [optional] delete building directories for smaller image sizes
 RUN rm -rf polyml-5.9*
 RUN rm -rf mosml-ver-2.10.1*
+RUN rm -rf opentheory-1.5*