From 65fd21fbcda2c22df440e4905e0559cde983f576 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] 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