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.

Author: fdupress

.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]