Updated Docker CI workflow with SMT solvers (HolSmt)

.github/workflows/docker-ci-for-pr.yml

@@ -24,6 +24,8 @@ jobs:
           push: false
           build-args: |
             SML=poly
+            Z3_VERSION=2.19
+            CVC_VERSION=5
             BUILDOPTS=--stdknl -j2 -t
 
   build-expk:
@@ -43,4 +45,6 @@ jobs:
           push: false
           build-args: |
             SML=poly
+            Z3_VERSION=2.19
+            CVC_VERSION=5
             BUILDOPTS=--expk -j2 -t

.github/workflows/docker-ci.yml

@@ -42,6 +42,8 @@ jobs:
           push: true
           build-args: |
             SML=poly
+            Z3_VERSION=2.19
+            CVC_VERSION=5
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--stdknl -j2 -t
           tags: ${{ steps.meta.outputs.tags }}
@@ -78,6 +80,8 @@ jobs:
           push: true
           build-args: |
             SML=poly
+            Z3_VERSION=2.19
+            CVC_VERSION=5
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--expk -j2 -t
           tags: ${{ steps.meta.outputs.tags }}

.github/workflows/self-runner.yml

@@ -12,7 +12,7 @@ on:
       kernel:
         description: 'HOL kernel'
         required: true
-        default: 'stdknl'
+        default: 'expk'
         type: choice
         options:
         - stdknl
@@ -35,8 +35,34 @@ on:
       more-options:
         description: 'More options'
         required: false
+        default: '-t'
         type: string
-
+      Z3:
+        description: 'Z3 version'
+        required: false
+        default: '4.12.4'
+        type: choice
+        options:
+        - ''
+        - 2.19
+        - 2.19.1
+        - 4.12.4
+      CVC:
+        description: 'CVC version'
+        required: false
+        default: '5'
+        type: choice
+        options:
+        - ''
+        - 5
+      Yices:
+        description: 'Yices verison'
+        required: false
+        default: ''
+        type: choice
+        options:
+        - ''
+        - 1.0.40
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -76,6 +102,9 @@ jobs:
             TARGETPLATFORM=${{ github.event.inputs.platform || env.default_platform }}
             # NOTE: mosml is too slow to be chosen here
             SML=poly
+            Z3_VERSION=${{ github.event.inputs.Z3 }}
+            CVC_VERSION=${{ github.event.inputs.CVC }}
+            YICES_VERSION=${{ github.event.inputs.Yices }}
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--${{ github.event.inputs.kernel || env.default_kernel }} -j${{ github.event.inputs.concurrency || env.default_concurrency }} ${{ github.event.inputs.more-options }}
           tags: ${{ steps.meta.outputs.tags }}

developers/docker-ci/Dockerfile

@@ -2,6 +2,7 @@
 #
 # HOL4 building environment (Docker), the CI image
 #
+# NOTE: this docker image is NOT for HOL developers to use interactively.
 
 # This "base" image is described in "base/Dockerfile"
 FROM --platform=$TARGETPLATFORM binghelisp/hol-dev:latest
@@ -20,6 +21,34 @@ WORKDIR /ML/HOL
 # fast copy all files to the docker image
 COPY --link . .
 
+ARG Z3_VERSION
+ARG CVC_VERSION
+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
+
 # building HOL
 RUN ${SML} < tools/smart-configure.sml 
 RUN bin/build ${BUILDOPTS}

developers/docker-ci/base/Dockerfile

@@ -10,6 +10,7 @@ FROM --platform=$TARGETPLATFORM debian:stable
 # The following two arguments are supported by "docker buildx"
 ARG TARGETPLATFORM
 ARG BUILDPLATFORM
+ARG POLY_VERSION="5.9.1"
 
 RUN echo "I was running on $BUILDPLATFORM, building for $TARGETPLATFORM" > /tmp/log
 
@@ -27,53 +28,46 @@ RUN apt-get install -qy build-essential graphviz git libgmp-dev wget curl procps
 
 # for Unicode display, learnt from Magnus Myreen
 RUN apt-get install -qy locales-all terminfo man aptitude
-RUN apt-get clean
-
-# IDE
-RUN apt-get install -qy emacs-nox
 
 # 1. install Moscow ML (https://github.com/kfl/mosml.git)
 RUN wget -q -O - https://github.com/kfl/mosml/archive/refs/tags/ver-2.10.1.tar.gz | tar xzf -
 RUN make -C mosml-ver-2.10.1/src world install
 RUN rm -rf mosml-ver-2.10.1
 
 # 2. install polyml (https://github.com/polyml/polyml.git)
-RUN wget -q -O polyml-master.zip https://github.com/polyml/polyml/archive/refs/heads/master.zip
-RUN unzip polyml-master.zip
+RUN wget -q -O polyml-${POLY_VERSION}.tar.gz \
+    https://github.com/polyml/polyml/archive/refs/tags/v${POLY_VERSION}.tar.gz
+RUN tar xzf polyml-${POLY_VERSION}.tar.gz
 RUN if [ "linux/386" = "$TARGETPLATFORM" ]; then \
-       cd polyml-master && ./configure --build=i686-pc-linux-gnu --enable-intinf-as-int; \
+       cd polyml-${POLY_VERSION} && ./configure --build=i686-pc-linux-gnu --enable-intinf-as-int; \
     else \
-       cd polyml-master && ./configure --enable-intinf-as-int; \
+       cd polyml-${POLY_VERSION} && ./configure --enable-intinf-as-int; \
     fi
-RUN make -C polyml-master -j4
-RUN make -C polyml-master compiler install
-RUN rm -rf polyml-master polyml-master.zip
+RUN make -C polyml-${POLY_VERSION} -j4
+RUN make -C polyml-${POLY_VERSION} install
+RUN rm -rf polyml-${POLY_VERSION} polyml-${POLY_VERSION}.tar.gz
 
 # 3. install MLton binary (https://github.com/MLton/mlton.git) for linux/amd64 only
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
     wget -q -O - https://github.com/MLton/mlton/releases/download/on-20210117-release/mlton-20210117-1.amd64-linux-glibc2.31.tgz | tar xzf -; fi
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then make -C mlton-20210117-1.amd64-linux-glibc2.31; fi
 RUN rm -rf mlton-20210117-1.amd64-linux-glibc2.31
 
-# 4. install OpenTheory with local packages
-RUN wget -q -O - https://github.com/binghe/opentheory/archive/refs/tags/v1.5.tar.gz | tar xzf -
+# 4. install OpenTheory (develop version)
+RUN wget -q -O opentheory-develop.zip \
+    https://github.com/binghe/opentheory/archive/refs/heads/develop.zip && unzip opentheory-develop.zip
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
-        make -C opentheory-1.5 mlton; \
+        make -C opentheory-develop mlton; \
     else \
-        make -C opentheory-1.5 polyml; \
+        make -C opentheory-develop polyml; \
     fi
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
-        cp opentheory-1.5/bin/mlton/opentheory /usr/local/bin; \
+        cp opentheory-develop/bin/mlton/opentheory /usr/local/bin; \
     else \
-        cp opentheory-1.5/bin/polyml/opentheory /usr/local/bin; \
+        cp opentheory-develop/bin/polyml/opentheory /usr/local/bin; \
     fi
-RUN rm -rf opentheory-1.5
-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 && rm opentheory-local.tar.gz
-
-# for HOL Emacs mode (Emacs is not installed by default, however)
-COPY .emacs /root
+RUN rm -rf opentheory-develop opentheory-develop.zip
+RUN opentheory init && opentheory install base
 
 ENV LANG en_US.UTF-8
 ENV LANGUAGE en_US:en

developers/docker-ci/base/Makefile

@@ -1,26 +1,14 @@
-# NOTE: If you meet "ERROR: failed to solve: no match for platform in manifest",
-#       your error should be related to this open issue [1] that enter into
-#       Docker Desktop 4.20.  As a workaround, you should disable the flag
-#      'Use containerd' for pulling and storing images within the feature of
-#       Docker Desktop to solve it [2].  -- Chun Tian (binghe), July 17, 2023
-#
-# [1] https://github.com/moby/moby/issues/44578
-# [2] https://stackoverflow.com/questions/76355896
-
-DOCKER_IMAGE=binghelisp/hol-dev
+DOCKER_IMAGE=binghelisp/hol-dev:base
 
 build:
 	docker buildx build --platform linux/386 .
 	docker buildx build --platform linux/amd64 .
 	docker buildx build --platform linux/arm64 .
-	docker buildx build --platform linux/386,linux/amd64,linux/arm64 \
-		-t $(DOCKER_IMAGE) .
+	docker buildx build --platform linux/386,linux/amd64,linux/arm64 -t $(DOCKER_IMAGE) .
 
-# This will reuse the images built locally by the "build" target
-push:
-	docker buildx build --platform linux/386,linux/amd64,linux/arm64 \
-		-t $(DOCKER_IMAGE) --push .
+push: build
+	docker push $(DOCKER_IMAGE)
 
 # This runs the docker image in your native platform
 run:
-	docker run -ti --rm $(DOCKER_IMAGE)
+	docker run -ti -v ML --rm $(DOCKER_IMAGE)