From 912baf6d5dd9b4882372781928b1f5306df2f9e8 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 28 Aug 2024 14:42:36 -0700 Subject: [PATCH 1/5] Update release OCaml version to 4.14 --- .docker/release.Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.docker/release.Dockerfile b/.docker/release.Dockerfile index 2cb9f4d9d64..f65adb03ef2 100644 --- a/.docker/release.Dockerfile +++ b/.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 From bc5917b04b5165ba286954f02b44884f0593dc27 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 28 Aug 2024 14:45:17 -0700 Subject: [PATCH 2/5] Use OCaml 4.14 in package dockerfile --- .docker/package.Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.docker/package.Dockerfile b/.docker/package.Dockerfile index efb429159af..7087f2e0e8c 100644 --- a/.docker/package.Dockerfile +++ b/.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 From ad4f8b5f3c51ea00d19865aca3ba863b91afc0e6 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 28 Aug 2024 12:55:54 -0700 Subject: [PATCH 3/5] Push image to ghcr.io --- .github/workflows/linux-x64-rebuild-base.yaml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.github/workflows/linux-x64-rebuild-base.yaml b/.github/workflows/linux-x64-rebuild-base.yaml index 6445ef96a25..1869d909414 100644 --- a/.github/workflows/linux-x64-rebuild-base.yaml +++ b/.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: | From bfc320f633099df59fad913ed038a915985ee314 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 28 Aug 2024 14:44:16 -0700 Subject: [PATCH 4/5] Use ghcr.io image in CI build --- .docker/standalone.Dockerfile | 2 +- .github/workflows/linux-x64.yaml | 13 +------------ 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/.docker/standalone.Dockerfile b/.docker/standalone.Dockerfile index 663ee4b824b..cce8b035c2b 100644 --- a/.docker/standalone.Dockerfile +++ b/.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. diff --git a/.github/workflows/linux-x64.yaml b/.github/workflows/linux-x64.yaml index 799c7502231..8cf8f838e99 100644 --- a/.github/workflows/linux-x64.yaml +++ b/.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 From feebd13ab7ee48a13aea5733c82cc45b0ea90755 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 28 Aug 2024 16:32:45 -0700 Subject: [PATCH 5/5] Make docker-ci pull the latest CI image. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 8e8e7f21f07..067836f4ca5 100644 --- a/Makefile +++ b/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 \ .