From af4b429b934a8acb14d41aea35933f0627d7b784 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Thu, 25 Apr 2024 18:40:21 +1000 Subject: [PATCH 1/5] Updated Dockerfiles with necessary TeXlive packages for building HOL manuals --- developers/docker-ci/Dockerfile | 7 +++++- developers/docker-ci/base/Dockerfile | 5 +++++ developers/docker-ci/base/Makefile | 2 +- developers/docker-ci/latest/Dockerfile | 31 +++++++++++++++++++++++--- developers/docker-ci/latest/Makefile | 2 +- 5 files changed, 41 insertions(+), 6 deletions(-) diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile index beb1df309a..b56f63070b 100644 --- a/developers/docker-ci/Dockerfile +++ b/developers/docker-ci/Dockerfile @@ -49,9 +49,14 @@ 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 \ + cd Manual && ../bin/Holmake -j2; \ +fi + # This can be overrided by "docker run " CMD ["/ML/HOL/bin/hol"] diff --git a/developers/docker-ci/base/Dockerfile b/developers/docker-ci/base/Dockerfile index 01641c16e9..2278d382d7 100644 --- 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 + # 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 index fecf173ae5..5ce3a6b1a1 100644 --- 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 index bcc90aa079..6d808eda5f 100644 --- 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 index 6605f246e5..a982ee4f4f 100644 --- 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 From 1e9ccf60f308417391fd53d1a8d769c3ca700512 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Thu, 25 Apr 2024 18:42:55 +1000 Subject: [PATCH 2/5] Update docker-ci-for-pr.yml (added build-mosml) --- .github/workflows/docker-ci-for-pr.yml | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker-ci-for-pr.yml b/.github/workflows/docker-ci-for-pr.yml index f01724e06e..74d59c8fce 100644 --- 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 From ab34d0b2169d530de58157a0b0689473f8586d86 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Thu, 25 Apr 2024 18:43:34 +1000 Subject: [PATCH 3/5] Update docker-ci.yml (add build-mosml) --- .github/workflows/docker-ci.yml | 40 +++++++++++++++++++++++++++++++-- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker-ci.yml b/.github/workflows/docker-ci.yml index ba9c1e9e49..8efa1a1735 100644 --- 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 }} From 57cde7241a028fa86c4f974ad509b70789cbba7a Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Thu, 25 Apr 2024 21:09:27 +1000 Subject: [PATCH 4/5] FTBFS with Moscow ML --- src/num/theories/cv_compute/automation/cv_memLib.sml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/num/theories/cv_compute/automation/cv_memLib.sml b/src/num/theories/cv_compute/automation/cv_memLib.sml index a8c97c34ac..002744b2d1 100644 --- 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 From b6defbe15ca1e6ebc6df3ecc01e69bd644a0b388 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Tue, 30 Apr 2024 18:49:16 +1000 Subject: [PATCH 5/5] Fixed building HOL manuals with PolyML (and not in --otknl) --- developers/docker-ci/Dockerfile | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile index b56f63070b..2851cab155 100644 --- a/developers/docker-ci/Dockerfile +++ b/developers/docker-ci/Dockerfile @@ -54,8 +54,12 @@ RUN ${SML} < tools/smart-configure.sml RUN bin/build ${BUILDOPTS} # Building HOL manuals when PolyML is used -RUN if [ "poly" == "${SML}"] ; then \ - cd Manual && ../bin/Holmake -j2; \ +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 "