HOL-Theorem-Prover · mn200 · May 3, 2024 · Apr 25, 2024 · Apr 25, 2024 · Apr 25, 2024
diff --git a/.github/workflows/docker-ci-for-pr.yml b/.github/workflows/docker-ci-for-pr.yml
@@ -24,7 +24,7 @@ jobs:
           push: false
           build-args: |
             SML=poly
-            Z3_VERSION=4.12.4
+            Z3_VERSION=4.13.0
             CVC_VERSION=5
             BUILDOPTS=--stdknl -j2 -t
 
@@ -45,6 +45,25 @@ jobs:
           push: false
           build-args: |
             SML=poly
-            Z3_VERSION=4.12.4
+            Z3_VERSION=4.13.0
             CVC_VERSION=5
             BUILDOPTS=--expk -j2 -t
+
+  build-mosml:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v3
+
+      - name: Build and push
+        uses: docker/build-push-action@v5
+        with:
+          context: .
+          file: developers/docker-ci/Dockerfile
+          push: false
+          build-args: |
+            SML=mosml
+            BUILDOPTS=--expk --seq=tools/sequences/upto-parallel -t
diff --git a/.github/workflows/docker-ci.yml b/.github/workflows/docker-ci.yml
@@ -42,7 +42,7 @@ jobs:
           push: true
           build-args: |
             SML=poly
-            Z3_VERSION=4.12.4
+            Z3_VERSION=4.13.0
             CVC_VERSION=5
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--stdknl -j2 -t
@@ -80,9 +80,45 @@ jobs:
           push: true
           build-args: |
             SML=poly
-            Z3_VERSION=4.12.4
+            Z3_VERSION=4.13.0
             CVC_VERSION=5
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--expk -j2 -t
           tags: ${{ steps.meta.outputs.tags }}
           labels: ${{ steps.meta.outputs.labels }}
+
+  build-mosml:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Docker meta
+        id: meta
+        uses: docker/metadata-action@v5
+        with:
+          images: ${{ env.USERNAME }}/hol-dev
+          tags: |
+            type=sha,prefix=ci-,suffix=-mosml
+
+      - name: Login to Docker Hub
+        uses: docker/login-action@v3
+        with:
+          username: ${{ env.USERNAME }}
+          password: ${{ env.PASSWORD }}
+
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v3
+
+      - name: Build and push
+        uses: docker/build-push-action@v5
+        with:
+          context: .
+          file: developers/docker-ci/Dockerfile
+          push: true
+          build-args: |
+            SML=mosml
+            # NOTE: the arg value cannot be quoted here:
+            BUILDOPTS=--expk --seq=tools/sequences/upto-parallel -t
+          tags: ${{ steps.meta.outputs.tags }}
+          labels: ${{ steps.meta.outputs.labels }}
diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
@@ -49,9 +49,18 @@ fi
 # remove potential local poly-includes.ML for docker builds
 RUN rm -f tools-poly/poly-includes.ML
 
-# building HOL
+# Building HOL itself
 RUN ${SML} < tools/smart-configure.sml 
 RUN bin/build ${BUILDOPTS}
 
+# Building HOL manuals when PolyML is used
+RUN if [ "poly" = "${SML}" ]; then \
+    if echo ${BUILDOPTS} | grep -q "otknl"; then \
+       echo Skip manual building; \
+    else \
+       cd Manual; ../bin/Holmake -j2; \
+    fi \
+fi
+
 # This can be overrided by "docker run <command>"
 CMD ["/ML/HOL/bin/hol"]
diff --git a/developers/docker-ci/base/Dockerfile b/developers/docker-ci/base/Dockerfile
@@ -7,6 +7,8 @@
 # GitHub Actions recommends Debian-based systems as base images
 FROM --platform=$TARGETPLATFORM debian:stable
 
+MAINTAINER Chun Tian <[email protected]>
+
 # The following two arguments are supported by "docker buildx"
 ARG TARGETPLATFORM
 ARG BUILDPLATFORM
@@ -29,6 +31,9 @@ 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
 
+# clean up downloaded packages after installation (this reduces Docker image sizes)
+RUN apt-get clean
+
 # 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

diff --git a/developers/docker-ci/base/Makefile b/developers/docker-ci/base/Makefile
@@ -6,7 +6,7 @@ build:
 	docker buildx build --platform linux/arm64 .
 	docker buildx build --platform linux/386,linux/amd64,linux/arm64 -t $(DOCKER_IMAGE) .
 
-push: build
+push:
 	docker push $(DOCKER_IMAGE)
 
 # This runs the docker image in your native platform

diff --git a/developers/docker-ci/latest/Dockerfile b/developers/docker-ci/latest/Dockerfile
@@ -30,8 +30,23 @@ RUN if [ "linux/amd64" = "$TARGETPLATFORM" ] || [ "linux/386" = "$TARGETPLATFORM
     rm z3-2.19.1.tar.gz; \
 fi
 
+# Z3 4.12.4
+RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
+    wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.12.4/z3-4.12.4-x64-glibc-2.35.zip; \
+    unzip z3-4.12.4-x64-glibc-2.35.zip; \
+    mv z3-4.12.4-x64-glibc-2.35 z3-4.12.4; \
+    rm z3-4.12.4-x64-glibc-2.35.zip; \
+fi
+
+RUN if [ "linux/arm64" = "$TARGETPLATFORM" ]; then \
+    wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.12.4/z3-4.12.4-arm64-glibc-2.35.zip; \
+    unzip z3-4.12.4-arm64-glibc-2.35.zip; \
+    mv z3-4.12.4-arm64-glibc-2.35 z3-4.12.4; \
+    rm z3-4.12.4-arm64-glibc-2.35.zip; \
+fi
+
 # Z3 4.x
-ARG Z3_VERSION="4.12.4"
+ARG Z3_VERSION="4.13.0"
 
 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; \
@@ -60,9 +75,14 @@ RUN if [ "linux/386" = "$TARGETPLATFORM" ]; then \
 fi
 
 # cvc5
+ARG CVC5_VERSION="1.1.2"
+
 RUN if [ "linux/amd64" = "$TARGETPLATFORM" ]; then \
-    wget -q https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux; \
-    chmod a+x cvc5-Linux; \
+    wget -q -O cvc5-Linux-static.zip \
+         https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux-static.zip; \
+    unzip cvc5-Linux-static.zip; \
+    rm cvc5-Linux-static.zip; \
+    ln -s cvc5-Linux-static/bin/cvc5 cvc5-Linux; \
 fi
 
 # NuRV 2.0.0
@@ -85,3 +105,8 @@ RUN if [ "linux/arm64" = "$TARGETPLATFORM" ]; then \
 fi
 
 ENV HOL4_SMV_EXECUTABLE=/ML/solvers/NuRV
+
+# necessary TeXlive packages for buliding HOL manuals (+pandoc for Markdown)
+RUN apt-get install -qy texlive-latex-recommended pandoc latexmk texlive-latex-extra \
+                        texlive-fonts-extra texlive-science
+RUN apt-get clean
diff --git a/developers/docker-ci/latest/Makefile b/developers/docker-ci/latest/Makefile
@@ -6,7 +6,7 @@ build:
 	docker buildx build --platform linux/arm64 .
 	docker buildx build --platform linux/386,linux/amd64,linux/arm64 -t $(DOCKER_IMAGE) .
 
-push: build
+push:
 	docker push $(DOCKER_IMAGE)
 
 # This runs the docker image in your native platform

diff --git a/src/num/theories/cv_compute/automation/cv_memLib.sml b/src/num/theories/cv_compute/automation/cv_memLib.sml
@@ -25,6 +25,7 @@ fun cv_print_term v tm = cv_print_aux v term_to_string tm;
 fun cv_print_thm v th = cv_print_aux v thm_to_string th;
 
 (* Custom version of Lib.time *)
+local open Time; in
 fun cv_time f x =
   let val start = Time.now()
       val res = f x
@@ -33,6 +34,7 @@ fun cv_time f x =
     cv_print Verbose ("Took " ^ Time.fmt 1 (finish - start) ^ " seconds.\n");
     res
   end
+end
 
 fun indent_print_aux f verbosity prefix suffix x = let
   val m = !max_print_depth