From 3deac1e5f29a4634b8ab90c89cec4e1ee527c3a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Thu, 7 May 2026 18:51:09 +0100 Subject: [PATCH 1/2] Refactor CI to run in fetch build box This refactors the CI jobs so compilation and checks (including external CI) run in a fresh build box. This will help ensure that changes to the box configuration (new dependencies, prover updates, prover additions, ...) are reflected quickly in the CI environment and can be leveraged in external proofs right away. The workflow is now: 1. Build base and build boxes, then save them as an artefact; 2. Recover the build box, then run the compilation check; 3. Recover the build box, then compile EasyCrypt and run a matrix check; (this recompiles EC 3 times in parallel, and likely needs changed) 4. Recover the build box, then compile EasyCrypt and run the external matrix checks (this recompiles EC as many times as we have external checks, and likely needs changed) 5. Build the test box, push the base and build boxes (all pushes) and the test box (release branches and tags) The nix compilation check is unchanged, notification fires after all succeed. Documentation is built as normal. --- .github/workflows/ci.yml | 203 ++++++++++++++++++++++++++--------- .github/workflows/docker.yml | 53 --------- 2 files changed, 152 insertions(+), 104 deletions(-) delete mode 100644 .github/workflows/docker.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 86a9f8b14..f5f1662de 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,32 +1,71 @@ -name: EasyCrypt compilation & check +name: EasyCrypt CI on: push: branches: - 'main' + - 'release' + - 'latest' + tags: + - 'r[0-9]+.[0-9]+' pull_request: merge_group: env: - HOME: /home/charlie - OPAMYES: true - OPAMJOBS: 2 + IMAGE_TAG: ci-${{ github.run_id }} jobs: + # ── Phase 1: Build Docker images and share via artifact ── + + docker: + name: Build Docker images + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + - name: Build base image + run: make -C scripts/docker build VARIANT=base TAG=$IMAGE_TAG + - name: Build build image + run: make -C scripts/docker build VARIANT=build TAG=$IMAGE_TAG + - name: Save images for downstream jobs + run: | + docker save "ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG" | gzip > base-image.tar.gz + docker save "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" | gzip > build-image.tar.gz + - uses: actions/upload-artifact@v4 + with: + name: docker-images + path: | + base-image.tar.gz + build-image.tar.gz + retention-days: 1 + + # ── Phase 2: CI ── + compile-opam: name: EasyCrypt compilation (opam) + needs: docker runs-on: ubuntu-24.04 - container: - image: ghcr.io/easycrypt/ec-build-box:main steps: - uses: actions/checkout@v4 - - name: Install EasyCrypt dependencies + - uses: actions/download-artifact@v4 + with: + name: docker-images + - run: gunzip -c build-image.tar.gz | docker load + - name: Install dependencies & compile run: | - opam pin add -n easycrypt . - opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt - opam install --deps-only easycrypt - - name: Compile EasyCrypt - run: opam exec -- make PROFILE=ci + docker run --rm \ + -v "$PWD:/workspace" \ + -w /workspace \ + -e HOME=/home/charlie \ + -e OPAMYES=true \ + -e OPAMJOBS=2 \ + "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ + bash -c " + set -e + opam pin add -n easycrypt . + opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt + opam install --deps-only easycrypt + opam exec -- make PROFILE=ci + " compile-nix: name: EasyCrypt compilation (nix) @@ -50,31 +89,38 @@ jobs: check: name: Check EasyCrypt Libraries - needs: compile-opam + needs: [docker, compile-opam] runs-on: ubuntu-24.04 - container: - image: ghcr.io/easycrypt/ec-build-box:main strategy: fail-fast: false matrix: target: [unit, stdlib, examples] steps: - uses: actions/checkout@v4 - - name: Install EasyCrypt dependencies - run: | - opam pin add -n easycrypt . - opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt - opam install --deps-only easycrypt - - name: Compile EasyCrypt - run: opam exec -- make - - name: Detect SMT provers + - uses: actions/download-artifact@v4 + with: + name: docker-images + - run: gunzip -c build-image.tar.gz | docker load + - name: Install, compile & test (${{ matrix.target }}) run: | - rm -f ~/.why3.conf - opam exec -- ./ec.native why3config -why3 ~/.why3.conf - - name: Compile Library (${{ matrix.target }}) - env: - TARGET: ${{ matrix.target }} - run: opam exec -- make $TARGET + docker run --rm \ + -v "$PWD:/workspace" \ + -w /workspace \ + -e HOME=/home/charlie \ + -e OPAMYES=true \ + -e OPAMJOBS=2 \ + -e TARGET=${{ matrix.target }} \ + "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ + bash -c " + set -e + opam pin add -n easycrypt . + opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt + opam install --deps-only easycrypt + opam exec -- make + rm -f ~/.why3.conf + opam exec -- ./ec.native why3config -why3 ~/.why3.conf + opam exec -- make \$TARGET + " - uses: actions/upload-artifact@v4 name: Upload report.log if: always() @@ -99,10 +145,8 @@ jobs: external: name: Check EasyCrypt External Projects - needs: [compile-opam, fetch-external-matrix] + needs: [docker, compile-opam, fetch-external-matrix] runs-on: ubuntu-24.04 - container: - image: ghcr.io/easycrypt/ec-build-box:main strategy: fail-fast: false matrix: @@ -112,8 +156,8 @@ jobs: with: path: easycrypt - name: Extract target branch name - run: echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT id: extract_branch + run: echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT - name: Find remote branch id: branch_name run: | @@ -128,25 +172,34 @@ jobs: -b ${{ steps.branch_name.outputs.REPO_BRANCH }} \ ${{ matrix.target.repository }} \ project/${{ matrix.target.name }} - - name: Install EasyCrypt dependencies - run: | - opam pin add -n easycrypt easycrypt - opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt - opam install --deps-only easycrypt - - name: Compile & Install EasyCrypt - run: opam exec -- make -C easycrypt build install - - name: Detect SMT provers - run: | - rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf - opam exec -- easycrypt why3config - - name: Compile project - working-directory: project/${{ matrix.target.name }}/${{ matrix.target.subdir }} + - uses: actions/download-artifact@v4 + with: + name: docker-images + - run: gunzip -c build-image.tar.gz | docker load + - name: Install, compile & test external project run: | - opam exec -- easycrypt runtest \ - -report report.log \ - ${{ matrix.target.options }} \ - ${{ matrix.target.config }} \ - ${{ matrix.target.scenario }} + docker run --rm \ + -v "$PWD:/workspace" \ + -w /workspace \ + -e HOME=/home/charlie \ + -e OPAMYES=true \ + -e OPAMJOBS=2 \ + "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ + bash -c " + set -e + opam pin add -n easycrypt easycrypt + opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt + opam install --deps-only easycrypt + opam exec -- make -C easycrypt build install + rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf + opam exec -- easycrypt why3config + cd project/${{ matrix.target.name }}/${{ matrix.target.subdir }} + opam exec -- easycrypt runtest \ + -report report.log \ + ${{ matrix.target.options }} \ + ${{ matrix.target.config }} \ + ${{ matrix.target.scenario }} + " - name: Compute real-path to report.log if: always() run: | @@ -170,6 +223,54 @@ jobs: jobs: ${{ toJSON(needs) }} allowed-skips: external + # ── Phase 3: Publish to GHCR (only on push after CI passes) ── + + 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') + ) + needs: [compile-opam, compile-nix, check, external, external-status, docker] + runs-on: ubuntu-24.04 + permissions: + packages: write + steps: + - uses: actions/checkout@v4 + - uses: actions/download-artifact@v4 + with: + name: docker-images + - run: gunzip -c base-image.tar.gz | docker load + - run: gunzip -c build-image.tar.gz | docker load + - uses: docker/login-action@v3 + with: + registry: ghcr.io + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} + - name: Push base image + run: | + docker tag "ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG" \ + "ghcr.io/easycrypt/ec-base-box:${{ github.ref_name }}" + docker push "ghcr.io/easycrypt/ec-base-box:${{ github.ref_name }}" + - name: Push build image + run: | + docker tag "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ + "ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }}" + docker push "ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }}" + - name: Build and push test image + if: | + github.ref == 'refs/heads/release' || + 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 }} + + # ── Notification ── + notification: name: Notification needs: [compile-opam, compile-nix, check, external, external-status] diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml deleted file mode 100644 index 8fb0e4730..000000000 --- a/.github/workflows/docker.yml +++ /dev/null @@ -1,53 +0,0 @@ -name: EasyCrypt Docker Containers Build - -on: - push: - branches: - - 'main' - - 'release' - tags: - - 'r[0-9]+.[0-9]+' - workflow_dispatch: - -jobs: - make-images: - name: Build and Push Container Images - runs-on: ubuntu-24.04 - permissions: - packages: write - env: - TAG: ${{ github.ref_name }} - steps: - - uses: actions/checkout@v4 - - - name: Log in to the Container registry - uses: docker/login-action@65b78e6e13532edd9afa3aa52ac7964289d1a9c1 - with: - registry: https://ghcr.io - username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} - - - name: Build and push `base` Image - env: - VARIANT: base - run: | - make -C scripts/docker build publish - - - name: Build and push `build` Image - env: - VARIANT: build - run: | - make -C scripts/docker build publish - - - name: Build and push `formosa` Image - env: - VARIANT: formosa - run: | - make -C scripts/docker build publish - - - name: Build and push `test` Image - if: github.ref_name != 'main' - env: - VARIANT: test - run: | - make -C scripts/docker build publish From c131c245b5550d5e0f3d33b52a1949709b7507f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Fri, 8 May 2026 11:37:32 +0100 Subject: [PATCH 2/2] consolidate builds --- .github/workflows/ci.yml | 180 +++++++++++++++------------------------ scripts/docker/Makefile | 3 +- 2 files changed, 73 insertions(+), 110 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f5f1662de..0870d36fb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,59 +13,51 @@ on: env: IMAGE_TAG: ci-${{ github.run_id }} + OPAMYES: true + OPAMJOBS: 2 jobs: - # ── Phase 1: Build Docker images and share via artifact ── + # ── Phase 1: Build and push all Docker images ── docker: - name: Build Docker images + name: Build and push Docker images runs-on: ubuntu-24.04 + permissions: + packages: write steps: - uses: actions/checkout@v4 - - name: Build base image - run: make -C scripts/docker build VARIANT=base TAG=$IMAGE_TAG - - name: Build build image - run: make -C scripts/docker build VARIANT=build TAG=$IMAGE_TAG - - name: Save images for downstream jobs - run: | - docker save "ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG" | gzip > base-image.tar.gz - docker save "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" | gzip > build-image.tar.gz - - uses: actions/upload-artifact@v4 + - uses: docker/login-action@v3 with: - name: docker-images - path: | - base-image.tar.gz - build-image.tar.gz - retention-days: 1 + registry: ghcr.io + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} + - name: Build and push base image + run: | + make -C scripts/docker build publish VARIANT=base TAG=$IMAGE_TAG + - name: Build and push build image + run: | + make -C scripts/docker build publish VARIANT=build TAG=$IMAGE_TAG + - name: Build and push test image + run: | + make -C scripts/docker build publish VARIANT=test TAG=$IMAGE_TAG VERSION=${{ github.head_ref || github.ref_name }} - # ── Phase 2: CI ── + # ── Phase 2: Compile CI profile in build box ── compile-opam: name: EasyCrypt compilation (opam) needs: docker runs-on: ubuntu-24.04 + container: + image: ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG steps: - uses: actions/checkout@v4 - - uses: actions/download-artifact@v4 - with: - name: docker-images - - run: gunzip -c build-image.tar.gz | docker load - - name: Install dependencies & compile + - name: Install EasyCrypt dependencies run: | - docker run --rm \ - -v "$PWD:/workspace" \ - -w /workspace \ - -e HOME=/home/charlie \ - -e OPAMYES=true \ - -e OPAMJOBS=2 \ - "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ - bash -c " - set -e - opam pin add -n easycrypt . - opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt - opam install --deps-only easycrypt - opam exec -- make PROFILE=ci - " + opam pin add -n easycrypt . + opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt + opam install --deps-only easycrypt + - name: Compile EasyCrypt + run: opam exec -- make PROFILE=ci compile-nix: name: EasyCrypt compilation (nix) @@ -87,40 +79,28 @@ jobs: run: | make nix-build-with-provers + # ── Phase 3: Test in test box (no rebuild) ── + check: name: Check EasyCrypt Libraries - needs: [docker, compile-opam] + needs: docker runs-on: ubuntu-24.04 + container: + image: ghcr.io/easycrypt/ec-test-box:$IMAGE_TAG strategy: fail-fast: false matrix: target: [unit, stdlib, examples] steps: - uses: actions/checkout@v4 - - uses: actions/download-artifact@v4 - with: - name: docker-images - - run: gunzip -c build-image.tar.gz | docker load - - name: Install, compile & test (${{ matrix.target }}) + - name: Detect SMT provers run: | - docker run --rm \ - -v "$PWD:/workspace" \ - -w /workspace \ - -e HOME=/home/charlie \ - -e OPAMYES=true \ - -e OPAMJOBS=2 \ - -e TARGET=${{ matrix.target }} \ - "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ - bash -c " - set -e - opam pin add -n easycrypt . - opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt - opam install --deps-only easycrypt - opam exec -- make - rm -f ~/.why3.conf - opam exec -- ./ec.native why3config -why3 ~/.why3.conf - opam exec -- make \$TARGET - " + rm -f ~/.why3.conf + opam exec -- easycrypt why3config -why3 ~/.why3.conf + - name: Compile Library (${{ matrix.target }}) + env: + TARGET: ${{ matrix.target }} + run: opam exec -- easycrypt runtest config/tests.config $TARGET - uses: actions/upload-artifact@v4 name: Upload report.log if: always() @@ -145,8 +125,10 @@ jobs: external: name: Check EasyCrypt External Projects - needs: [docker, compile-opam, fetch-external-matrix] + needs: [docker, fetch-external-matrix] runs-on: ubuntu-24.04 + container: + image: ghcr.io/easycrypt/ec-test-box:$IMAGE_TAG strategy: fail-fast: false matrix: @@ -156,8 +138,8 @@ jobs: with: path: easycrypt - name: Extract target branch name - id: extract_branch run: echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT + id: extract_branch - name: Find remote branch id: branch_name run: | @@ -172,34 +154,18 @@ jobs: -b ${{ steps.branch_name.outputs.REPO_BRANCH }} \ ${{ matrix.target.repository }} \ project/${{ matrix.target.name }} - - uses: actions/download-artifact@v4 - with: - name: docker-images - - run: gunzip -c build-image.tar.gz | docker load - - name: Install, compile & test external project + - name: Detect SMT provers + run: | + rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf + opam exec -- easycrypt why3config + - name: Compile project + working-directory: project/${{ matrix.target.name }}/${{ matrix.target.subdir }} run: | - docker run --rm \ - -v "$PWD:/workspace" \ - -w /workspace \ - -e HOME=/home/charlie \ - -e OPAMYES=true \ - -e OPAMJOBS=2 \ - "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ - bash -c " - set -e - opam pin add -n easycrypt easycrypt - opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt - opam install --deps-only easycrypt - opam exec -- make -C easycrypt build install - rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf - opam exec -- easycrypt why3config - cd project/${{ matrix.target.name }}/${{ matrix.target.subdir }} - opam exec -- easycrypt runtest \ - -report report.log \ - ${{ matrix.target.options }} \ - ${{ matrix.target.config }} \ - ${{ matrix.target.scenario }} - " + opam exec -- easycrypt runtest \ + -report report.log \ + ${{ matrix.target.options }} \ + ${{ matrix.target.config }} \ + ${{ matrix.target.scenario }} - name: Compute real-path to report.log if: always() run: | @@ -223,7 +189,7 @@ jobs: jobs: ${{ toJSON(needs) }} allowed-skips: external - # ── Phase 3: Publish to GHCR (only on push after CI passes) ── + # ── Phase 4: Retag and push with permanent tags ── publish: name: Publish Docker images @@ -239,37 +205,33 @@ jobs: permissions: packages: write steps: - - uses: actions/checkout@v4 - - uses: actions/download-artifact@v4 - with: - name: docker-images - - run: gunzip -c base-image.tar.gz | docker load - - run: gunzip -c build-image.tar.gz | docker load - uses: docker/login-action@v3 with: registry: ghcr.io username: ${{ github.actor }} password: ${{ secrets.GITHUB_TOKEN }} - - name: Push base image + - name: Pull and retag base image run: | - docker tag "ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG" \ - "ghcr.io/easycrypt/ec-base-box:${{ github.ref_name }}" - docker push "ghcr.io/easycrypt/ec-base-box:${{ github.ref_name }}" - - name: Push build image + docker pull ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG + docker tag ghcr.io/easycrypt/ec-base-box:$IMAGE_TAG \ + ghcr.io/easycrypt/ec-base-box:${{ github.ref_name }} + docker push ghcr.io/easycrypt/ec-base-box:${{ github.ref_name }} + - name: Pull and retag build image run: | - docker tag "ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG" \ - "ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }}" - docker push "ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }}" - - name: Build and push test image + docker pull ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG + docker tag ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG \ + ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }} + docker push ghcr.io/easycrypt/ec-build-box:${{ github.ref_name }} + - name: Pull and retag test image if: | github.ref == 'refs/heads/release' || 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 }} - - # ── Notification ── + docker pull ghcr.io/easycrypt/ec-test-box:$IMAGE_TAG + docker tag ghcr.io/easycrypt/ec-test-box:$IMAGE_TAG \ + ghcr.io/easycrypt/ec-test-box:${{ github.ref_name }} + docker push ghcr.io/easycrypt/ec-test-box:${{ github.ref_name }} notification: name: Notification diff --git a/scripts/docker/Makefile b/scripts/docker/Makefile index 1ca81eb28..7900c3a56 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