Refactor CI to run in fresh build box

.github/workflows/ci.yml

@@ -1,23 +1,54 @@
-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
+  IMAGE_TAG: ci-${{ github.run_id }}
   OPAMYES: true
   OPAMJOBS: 2
 
 jobs:
+  # ── Phase 1: Build and push all Docker images ──
+
+  docker:
+    name: Build and push Docker images
+    runs-on: ubuntu-24.04
+    permissions:
+      packages: write
+    steps:
+    - uses: actions/checkout@v4
+    - uses: docker/login-action@v3
+      with:
+        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
+
+  # ── 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:main
+      image: ghcr.io/easycrypt/ec-build-box:$IMAGE_TAG
     steps:
     - uses: actions/checkout@v4
     - name: Install EasyCrypt dependencies
@@ -48,33 +79,28 @@ jobs:
       run: |
         make nix-build-with-provers
 
+  # ── Phase 3: Test in test box (no rebuild) ──
+
   check:
     name: Check EasyCrypt Libraries
-    needs: compile-opam
+    needs: docker
     runs-on: ubuntu-24.04
     container:
-      image: ghcr.io/easycrypt/ec-build-box:main
+      image: ghcr.io/easycrypt/ec-test-box:$IMAGE_TAG
     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
       run: |
         rm -f ~/.why3.conf
-        opam exec -- ./ec.native why3config -why3 ~/.why3.conf
+        opam exec -- easycrypt why3config -why3 ~/.why3.conf
     - name: Compile Library (${{ matrix.target }})
       env:
         TARGET: ${{ matrix.target }}
-      run: opam exec -- make $TARGET
+      run: opam exec -- easycrypt runtest config/tests.config $TARGET
     - uses: actions/upload-artifact@v4
       name: Upload report.log
       if: always()
@@ -99,10 +125,10 @@ jobs:
 
   external:
     name: Check EasyCrypt External Projects
-    needs: [compile-opam, fetch-external-matrix]
+    needs: [docker, fetch-external-matrix]
     runs-on: ubuntu-24.04
     container:
-      image: ghcr.io/easycrypt/ec-build-box:main
+      image: ghcr.io/easycrypt/ec-test-box:$IMAGE_TAG
     strategy:
       fail-fast: false
       matrix:
@@ -128,13 +154,6 @@ 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
@@ -170,6 +189,50 @@ jobs:
         jobs: ${{ toJSON(needs) }}
         allowed-skips: external
 
+  # ── Phase 4: Retag and push with permanent tags ──
+
+  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: docker/login-action@v3
+      with:
+        registry: ghcr.io
+        username: ${{ github.actor }}
+        password: ${{ secrets.GITHUB_TOKEN }}
+    - name: Pull and retag base image
+      run: |
+        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 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: |
+        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
     needs: [compile-opam, compile-nix, check, external, external-status]