From 58554e61464f45b8ad586e4d95a12b5ad9ddfe9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 13 May 2026 21:53:29 +0100 Subject: [PATCH 1/2] [docker] consolidate dockerfiles MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This allows us to parameterise later layers on earlier ones. In practice, I want to use this to avoid rebuilding the `base` layer in PR and merge queue runs, building it only on `main` and release branches and tags. As a drive-by bonus, this means we can cache the `base` and `build` layers for reuse when building the `test` layer. I've also added a hook to allow building from a local working copy. (By providing an EC_REPO argument when building the `test` target.) This should allow us to pre-build the test image once and for all for all post-build checks. (Using `.` as EC_REPO, perhaps—haven't really thought that far.) --- .../docker/{Dockerfile.build => Dockerfile} | 55 +++++++++++++++++-- scripts/docker/Dockerfile.base | 34 ------------ scripts/docker/Dockerfile.formosa | 7 --- scripts/docker/Dockerfile.test | 10 ---- scripts/docker/Makefile | 5 +- 5 files changed, 52 insertions(+), 59 deletions(-) rename scripts/docker/{Dockerfile.build => Dockerfile} (82%) delete mode 100644 scripts/docker/Dockerfile.base delete mode 100644 scripts/docker/Dockerfile.formosa delete mode 100644 scripts/docker/Dockerfile.test diff --git a/scripts/docker/Dockerfile.build b/scripts/docker/Dockerfile similarity index 82% rename from scripts/docker/Dockerfile.build rename to scripts/docker/Dockerfile index b7ea758111..50e3cbbcc7 100644 --- a/scripts/docker/Dockerfile.build +++ b/scripts/docker/Dockerfile @@ -1,6 +1,42 @@ -# syntax = devthefuture/dockerfile-x +ARG BASE_LAYER=base +ARG BUILD_LAYER=build -FROM ./Dockerfile.base as base-build +# Base environment +FROM debian:stable AS base + +LABEL org.opencontainers.image.maintainer="Pierre-Yves Strub " + +ARG user=charlie + +ENV DEBIAN_FRONTEND=noninteractive + +RUN \ + apt-get -q -y update && \ + apt-get -q -y upgrade && \ + apt-get -q -y install sudo && \ + apt-get -q -y clean + +COPY --chown=root:root --chmod=0400 docker-parts/sudoers /etc/sudoers.d/ + +RUN \ + useradd -ms /bin/bash -d /home/$user -g root -G sudo -u 1001 $user + +RUN \ + apt-get -q -y install opam && \ + apt-get -q -y clean + +USER $user +WORKDIR /home/$user + +ENV OPAMYES=true OPAMVERBOSE=0 OPAMJOBS=4 + +ARG OCAML_VERSION=4.14.2 + +RUN \ + opam init --disable-sandboxing --compiler=ocaml-base-compiler.${OCAML_VERSION} + +# Build environment +FROM ${BASE_LAYER} AS build RUN \ sudo apt-get -q -y install wget curl python3 python3-pip python3-yaml && \ @@ -42,8 +78,6 @@ RUN \ opam clean --switch=alt-ergo-${version} && \ ln -s run-alt-ergo ~/bin/alt-ergo-${version} -FROM base-build as main-linux-amd64 - RUN \ version=1.8 && \ wget -O cvc4 https://github.com/CVC4/CVC4-archived/releases/download/${version}/cvc4-${version}-x86_64-linux-opt && \ @@ -119,7 +153,16 @@ RUN \ sudo install -m 0755 z3 /usr/local/bin/z3-${version} && \ rm -f z3 z3.zip -FROM main-linux-amd64 - RUN \ opam exec -- why3 config detect + +# Test environment +FROM ${BUILD_LAYER} AS test + +ARG EC_VERSION=main +ARG EC_REPO=https://github.com/EasyCrypt/easycrypt.git#${EC_VERSION} + +RUN \ + opam pin add -n easycrypt ${EC_REPO} && \ + opam install -v easycrypt && \ + rm -rf .opam/packages.dev/* diff --git a/scripts/docker/Dockerfile.base b/scripts/docker/Dockerfile.base deleted file mode 100644 index 1a43903b01..0000000000 --- a/scripts/docker/Dockerfile.base +++ /dev/null @@ -1,34 +0,0 @@ -# syntax = devthefuture/dockerfile-x - -FROM debian:stable - -LABEL org.opencontainers.image.maintainer="Pierre-Yves Strub " - -ARG user=charlie - -ENV DEBIAN_FRONTEND=noninteractive - -RUN \ - apt-get -q -y update && \ - apt-get -q -y upgrade && \ - apt-get -q -y install sudo && \ - apt-get -q -y clean - -COPY --chown=root:root --chmod=0400 docker-parts/sudoers /etc/sudoers.d/ - -RUN \ - useradd -ms /bin/bash -d /home/$user -g root -G sudo -u 1001 $user - -RUN \ - apt-get -q -y install opam && \ - apt-get -q -y clean - -USER $user -WORKDIR /home/$user - -ENV OPAMYES=true OPAMVERBOSE=0 OPAMJOBS=4 - -ARG OCAML_VERSION=4.14.2 - -RUN \ - opam init --disable-sandboxing --compiler=ocaml-base-compiler.${OCAML_VERSION} diff --git a/scripts/docker/Dockerfile.formosa b/scripts/docker/Dockerfile.formosa deleted file mode 100644 index 8ff3767340..0000000000 --- a/scripts/docker/Dockerfile.formosa +++ /dev/null @@ -1,7 +0,0 @@ -# syntax = devthefuture/dockerfile-x - -FROM ./Dockerfile.build as build-formosa - -RUN \ - opam install --deps-only --confirm-level=unsafe-yes jasmin && \ - opam clean diff --git a/scripts/docker/Dockerfile.test b/scripts/docker/Dockerfile.test deleted file mode 100644 index 2e9522d3aa..0000000000 --- a/scripts/docker/Dockerfile.test +++ /dev/null @@ -1,10 +0,0 @@ -# syntax = devthefuture/dockerfile-x - -FROM ./Dockerfile.build - -ARG EC_VERSION=main - -RUN \ - opam pin add -n easycrypt https://github.com/EasyCrypt/easycrypt.git#${EC_VERSION} && \ - opam install -v easycrypt && \ - rm -rf .opam/packages.dev/* diff --git a/scripts/docker/Makefile b/scripts/docker/Makefile index 1ca81eb283..383c39702c 100644 --- a/scripts/docker/Makefile +++ b/scripts/docker/Makefile @@ -3,7 +3,8 @@ # -------------------------------------------------------------------- VARIANT ?= build TAG ?= main -BARGS += --build-arg EC_VERSION=$(TAG) +VERSION ?= $(TAG) +BARGS += --build-arg EC_VERSION=$(VERSION) # -------------------------------------------------------------------- .PHONY: default build publish @@ -11,7 +12,7 @@ BARGS += --build-arg EC_VERSION=$(TAG) default: build build: - docker build -f Dockerfile.$(VARIANT) \ + docker build --target $(VARIANT) \ --platform linux/amd64 \ $(BARGS) \ -t ghcr.io/easycrypt/ec-$(VARIANT)-box:$(TAG) \ From 69d119c3a9749e78013264c2463f3f32917be75b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Thu, 14 May 2026 18:33:28 +0100 Subject: [PATCH 2/2] [ci] do not rebuild base in PR runs Streamline the docker builds slightly - Use the last base box from `main` for PR and merge queue runs. Rebuild only on pushes to `main` and releases. - Reuses the already-built build box when building the test box. --- .github/workflows/ci.yml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f5f1662ded..dfe76fd2f0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,9 +23,15 @@ jobs: steps: - uses: actions/checkout@v4 - name: Build base image + if: github.event_name == 'push' run: make -C scripts/docker build VARIANT=base TAG=$IMAGE_TAG + - name: Retrieve base image + if: github.event_name == 'pull_request' || github.event_name == 'merge_group' + run: | + docker pull ghcr.io/easycrypt/ec-base-box:main + docker tag ghcr.io/easycrypt/ec-base-box:main ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG - name: Build build image - run: make -C scripts/docker build VARIANT=build TAG=$IMAGE_TAG + run: make -C scripts/docker build VARIANT=build TAG=$IMAGE_TAG BARGS='--build-arg BASE_LAYER=ghcr.io/easycrypt/ec-base-box:${IMAGE_TAG}' - name: Save images for downstream jobs run: | docker save "ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG" | gzip > base-image.tar.gz @@ -228,12 +234,7 @@ jobs: publish: name: Publish Docker images if: | - github.event_name == 'push' && ( - github.ref == 'refs/heads/main' || - github.ref == 'refs/heads/release' || - github.ref == 'refs/heads/latest' || - startsWith(github.ref, 'refs/tags/r') - ) + github.event_name == 'push' needs: [compile-opam, compile-nix, check, external, external-status, docker] runs-on: ubuntu-24.04 permissions: @@ -266,8 +267,7 @@ jobs: github.ref == 'refs/heads/latest' || github.ref_type == 'tag' run: | - make -C scripts/docker build VARIANT=test TAG=${{ github.ref_name }} - make -C scripts/docker publish VARIANT=test TAG=${{ github.ref_name }} + make -C scripts/docker build publish VARIANT=test TAG=${{ github.ref_name }} BARGS='--build-arg BUILD_LAYER=ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }}' # ── Notification ──