Updated "hol-dev:latest" with more solvers (SMV) installed; print SMT…

… solver versions into build logs
HOL-Theorem-Prover · Jan 16, 2024 · 083bf6e · 083bf6e
1 parent cd78400
commit 083bf6e
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 9 deletions.
diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
@@ -28,14 +28,23 @@ ARG YICES_VERSION
 # if --build-arg Z3_VERSION=2.19, set HOL4_Z3_EXECUTABLE to its full path,
 # or set to null otherwise.
 ENV HOL4_Z3_EXECUTABLE=${Z3_VERSION:+/ML/z3-${Z3_VERSION}/bin/z3}
+RUN if [ "" != "${Z3_VERSION}" ]; then \
+    echo "Using Z3 solver: `${HOL4_Z3_EXECUTABLE} -version`"; \
+fi
 
 # if --build-arg CVC_VERSION=5, set HOL4_CVC_EXECUTABLE to its full path,
 # or set to null otherwise.
 ENV HOL4_CVC_EXECUTABLE=${CVC_VERSION:+/ML/cvc${CVC_VERSION}-Linux}
+RUN if [ "" != "${CVC_VERSION}" ]; then \
+    echo "Using CVC solver: `${HOL4_CVC_EXECUTABLE} --version | head -1`"; \
+fi
 
 # if --build-arg YICES_VERSION=1.0.40, set HOL4_YICES_EXECUTABLE to its full path,
 # or set to null otherwise.
 ENV HOL4_YICES_EXECUTABLE=${YICES_VERSION:+/ML/yices-${YICES_VERSION}/bin/yices}
+RUN if [ "" != "${YICES_VERSION}" ]; then \
+    echo "Using Yices solver: `${HOL4_YICES_EXECUTABLE} --version`"; \
+fi
 
 # remove potential local poly-includes.ML for docker builds
 RUN rm -f tools-poly/poly-includes.ML

diff --git a/developers/docker-ci/latest/Dockerfile b/developers/docker-ci/latest/Dockerfile
@@ -15,26 +15,19 @@ RUN echo "I was running on $BUILDPLATFORM, building for $TARGETPLATFORM" > /tmp/
 
 WORKDIR /ML
 
-# Use this mode when you need zero interaction while installing or upgrading the system via apt
-ENV DEBIAN_FRONTEND=noninteractive
-ENV LD_LIBRARY_PATH=/usr/local/lib
-ENV PATH=/ML/HOL/bin:$PATH
-
-ENV LANG en_US.UTF-8
-ENV LANGUAGE en_US:en
-ENV LC_ALL en_US.UTF-8
-
 # Z3 2.19 and 2.19.1
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ] || [ "linux/386" = "$TARGETPLATFORM" ]; then \
     wget -q -O z3-2.19.tar.gz https://github.com/Z3Prover/bin/raw/master/legacy/z3-2.19.tar.gz; \
     tar xzf z3-2.19.tar.gz; \
     mv z3 z3-2.19; \
+    rm z3-2.19.tar.gz; \
 fi
 
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ] || [ "linux/386" = "$TARGETPLATFORM" ]; then \
     wget -q -O z3-2.19.1.tar.gz https://github.com/Z3Prover/bin/raw/master/legacy/z3-2.19.1.tar.gz; \
     tar xzf z3-2.19.1.tar.gz; \
     mv z3 z3-2.19.1; \
+    rm z3-2.19.1.tar.gz; \
 fi
 
 # Z3 4.x
@@ -44,26 +37,51 @@ RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
     wget -q https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-glibc-2.35.zip; \
     unzip z3-${Z3_VERSION}-x64-glibc-2.35.zip; \
     mv z3-${Z3_VERSION}-x64-glibc-2.35 z3-${Z3_VERSION}; \
+    rm z3-${Z3_VERSION}-x64-glibc-2.35.zip; \
 fi
 
 RUN if [ "linux/arm64" = "$TARGETPLATFORM" ]; then \
     wget -q https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-arm64-glibc-2.35.zip; \
     unzip z3-${Z3_VERSION}-arm64-glibc-2.35.zip; \
     mv z3-${Z3_VERSION}-arm64-glibc-2.35 z3-${Z3_VERSION}; \
+    rm z3-${Z3_VERSION}-arm64-glibc-2.35.zip; \
 fi
 
 # Yices 1.0.40
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
     wget -q https://yices.csl.sri.com/old/binaries/yices-1.0.40-x86_64-unknown-linux-gnu-static-gmp.tar.gz; \
     tar xzf yices-1.0.40-x86_64-unknown-linux-gnu-static-gmp.tar.gz; \
+    rm yices-1.0.40-x86_64-unknown-linux-gnu-static-gmp.tar.gz; \
 fi
 RUN if [ "linux/386" = "$TARGETPLATFORM" ]; then \
     wget -q https://yices.csl.sri.com/old/binaries/yices-1.0.40-i686-pc-linux-gnu-static-gmp.tar.gz; \
     tar xzf yices-1.0.40-i686-pc-linux-gnu-static-gmp.tar.gz; \
+    rm yices-1.0.40-i686-pc-linux-gnu-static-gmp.tar.gz; \
 fi
 
 # cvc5
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
     wget -q https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux; \
     chmod a+x cvc5-Linux; \
 fi
+
+# NuRV 2.0.0
+ARG SMV_VERSION="2.0.0"
+
+RUN mkdir -p solvers
+
+RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
+    wget -q https://es-static.fbk.eu/tools/nurv/releases/NuRV-${SMV_VERSION}-linuxx64.tar.bz2; \
+    tar xjf NuRV-${SMV_VERSION}-linuxx64.tar.bz2; \
+    mv NuRV-${SMV_VERSION}-linuxx64/NuRV solvers; \
+    rm -rf NuRV-${SMV_VERSION}-linuxx64*; \
+fi
+
+RUN if [ "linux/arm64" = "$TARGETPLATFORM" ]; then \
+    wget -q https://es-static.fbk.eu/tools/nurv/releases/NuRV-${SMV_VERSION}-linuxarm64.tar.bz2; \
+    tar xjf NuRV-${SMV_VERSION}-linuxarm64.tar.bz2; \
+    mv NuRV-${SMV_VERSION}-linuxarm64/NuRV solvers; \
+    rm -rf NuRV-${SMV_VERSION}-linuxx64*; \
+fi
+
+ENV HOL4_SMV_EXECUTABLE=/ML/solvers/NuRV