Push CI images to ghcr.io

.docker/package.Dockerfile

@@ -1,7 +1,7 @@
 # This Dockerfile should be run from the root FStar directory
 
 # Build the package
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 ARG CI_THREADS=24
 
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild

.docker/release.Dockerfile

@@ -1,7 +1,7 @@
 # This Dockerfile should be run from the root FStar directory
 
 # Build the package
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 ARG CI_THREADS=24
 
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild

.docker/standalone.Dockerfile

@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root FStar directory
 
-ARG FSTAR_CI_BASE=fstar_ci_base
+ARG FSTAR_CI_BASE=ghcr.io/fstarlang/fstar-ci-base
 FROM ${FSTAR_CI_BASE}
 
 # Copy repo into image.

.github/workflows/linux-x64-rebuild-base.yaml

@@ -50,6 +50,16 @@ jobs:
         run: |
           docker tag ${TEMP_IMAGE_NAME} fstar_ci_base
 
+      - name: Push base image
+        if: ${{ (success () && github.ref_name == 'master') || inputs.force }}
+        run: |
+          echo "$GITHUB_TOKEN" | docker login ghcr.io -u ${{ github.actor }} --password-stdin
+          docker tag ${TEMP_IMAGE_NAME} ghcr.io/fstarlang/fstar-ci-base:latest
+          docker push ghcr.io/fstarlang/fstar-ci-base:latest
+          docker logout ghcr.io
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
       - name: Compute elapsed time and status message
         if: ${{ always() }}
         run: |

.github/workflows/linux-x64.yaml

@@ -56,22 +56,11 @@ jobs:
         run: |
           echo "RESOURCEMONITOR=1" >> $GITHUB_ENV
 
-      - name: Make sure base image is present, or build it
-        run: |
-          if ! docker images | grep '^fstar_ci_base '; then
-            echo '*** REBUILDING fstar_ci_base image'
-            CI_IMAGEBUILD_INITIAL_TIMESTAMP=$(date '+%s')
-            docker build -f .docker/base.Dockerfile -t fstar_ci_base .
-            CI_IMAGEBUILD_FINAL_TIMESTAMP=$(date '+%s')
-            echo "CI_IMAGEBUILD_INITIAL_TIMESTAMP=$CI_IMAGEBUILD_INITIAL_TIMESTAMP" >> $GITHUB_ENV
-            echo "CI_IMAGEBUILD_FINAL_TIMESTAMP=$CI_IMAGEBUILD_FINAL_TIMESTAMP" >> $GITHUB_ENV
-          fi
-
       - name: Build FStar and its dependencies
         run: |
           ci_docker_image_tag=fstar:local-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
           echo "ci_docker_image_tag=$ci_docker_image_tag" >> $GITHUB_ENV
-          docker build -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_RECORD_HINTS_ARG $CI_DO_NO_KARAMEL . |& tee BUILDLOG
+          docker build --pull -t $ci_docker_image_tag -f .docker/standalone.Dockerfile --build-arg CI_BRANCH=$GITHUB_REF_NAME --build-arg RESOURCEMONITOR=$RESOURCEMONITOR --build-arg CI_THREADS=$(nproc) $CI_RECORD_HINTS_ARG $CI_DO_NO_KARAMEL . |& tee BUILDLOG
           ci_docker_status=$(docker run $ci_docker_image_tag /bin/bash -c 'cat $FSTAR_HOME/status.txt' || echo false)
           if $ci_docker_status && [[ -z "$CI_SKIP_IMAGE_TAG" ]] ; then
             if ! { echo $GITHUB_REF_NAME | grep '/' ; } ; then

Makefile

@@ -173,7 +173,7 @@ ci:
 # CI.
 .PHONY: docker-ci
 docker-ci:
-	docker build -f .docker/standalone.Dockerfile \
+	docker build --pull -f .docker/standalone.Dockerfile \
 		--build-arg CI_THREADS=$(shell nproc) \
 		--build-arg FSTAR_CI_NO_GITDIFF=1 \
 		.