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 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 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-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: | 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 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 \ .