Refactor CI to run in fresh build box #4862
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: EasyCrypt CI | |
| on: | |
| push: | |
| branches: | |
| - 'main' | |
| - 'release' | |
| - 'latest' | |
| tags: | |
| - 'r[0-9]+.[0-9]+' | |
| pull_request: | |
| merge_group: | |
| env: | |
| 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 | |
| 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 | |
| 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 | |
| " | |
| compile-nix: | |
| name: EasyCrypt compilation (nix) | |
| env: | |
| HOME: /home/runner | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Setup Nix | |
| uses: cachix/install-nix-action@v26 | |
| with: | |
| nix_path: nixpkgs=channel:nixos-unstable | |
| - name: Setup Cachix | |
| uses: cachix/cachix-action@v14 | |
| with: | |
| name: formosa-crypto | |
| authToken: '${{ secrets.CACHIX_WRITE_TOKEN }}' | |
| - name: Build and cache EasyCrypt and dependencies | |
| run: | | |
| make nix-build-with-provers | |
| check: | |
| name: Check EasyCrypt Libraries | |
| needs: [docker, compile-opam] | |
| runs-on: ubuntu-24.04 | |
| 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 }}) | |
| 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 | |
| " | |
| - uses: actions/upload-artifact@v4 | |
| name: Upload report.log | |
| if: always() | |
| with: | |
| name: report.log (${{ matrix.target }}) | |
| path: report.log | |
| if-no-files-found: ignore | |
| fetch-external-matrix: | |
| name: Fetch EasyCrypt External Projects Matrix | |
| runs-on: ubuntu-24.04 | |
| outputs: | |
| matrix: ${{ steps.set-matrix.outputs.matrix }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| path: 'easycrypt' | |
| - id: set-matrix | |
| run: | | |
| JSON=$(jq -c . < easycrypt/.github/workflows/external.json) | |
| echo "matrix=${JSON}" >> $GITHUB_OUTPUT | |
| external: | |
| name: Check EasyCrypt External Projects | |
| needs: [docker, compile-opam, fetch-external-matrix] | |
| runs-on: ubuntu-24.04 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| target: ${{fromJson(needs.fetch-external-matrix.outputs.matrix)}} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| path: easycrypt | |
| - name: Extract target branch name | |
| id: extract_branch | |
| run: echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT | |
| - name: Find remote branch | |
| id: branch_name | |
| run: | | |
| git ls-remote --exit-code --heads ${{ matrix.target.repository }} refs/heads/${{ steps.extract_branch.outputs.branch }} || exists=$? | |
| if [ "$exists" = "2" ]; | |
| then echo "REPO_BRANCH=${{ matrix.target.branch }}" >> $GITHUB_OUTPUT; | |
| else echo "REPO_BRANCH=${{ steps.extract_branch.outputs.branch }}" >> $GITHUB_OUTPUT; | |
| fi | |
| - name: Checkout External Project | |
| run: | | |
| git clone --recurse-submodules \ | |
| -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 | |
| 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 }} | |
| " | |
| - name: Compute real-path to report.log | |
| if: always() | |
| run: | | |
| echo "report=$(realpath project/${{ matrix.target.name }}/${{ matrix.target.subdir }})/report.log" >> $GITHUB_ENV | |
| - uses: actions/upload-artifact@v4 | |
| name: Upload report.log | |
| if: always() | |
| with: | |
| name: report.log (${{ matrix.target.name }}) | |
| path: ${{ env.report }} | |
| if-no-files-found: ignore | |
| external-status: | |
| name: Check EasyCrypt External Projects (set-status) | |
| if: always() | |
| needs: [external] | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: re-actors/alls-green@release/v1 | |
| with: | |
| 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] | |
| if: | | |
| (github.event_name == 'push') || | |
| (github.event_name == 'pull_request' && github.event.pull_request.head.repo.full_name == github.repository) | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: technote-space/workflow-conclusion-action@v3 | |
| - uses: zulip/github-actions-zulip/send-message@v1 | |
| with: | |
| api-key: ${{ secrets.ZULIP_APIKEY }} | |
| email: ${{ secrets.ZULIP_EMAIL }} | |
| organization-url: 'https://formosa-crypto.zulipchat.com' | |
| type: 'stream' | |
| to: 'GitHub notifications' | |
| topic: 'EasyCrypt / CI' | |
| content: | | |
| **Build status**: ${{ env.WORKFLOW_CONCLUSION }} ${{ env.WORKFLOW_CONCLUSION == 'success' && ':check_mark:' || ':cross_mark:' }} | |
| **Author**: [${{ github.actor }}](${{ github.server_url }}/${{ github.actor }}) | |
| **Event**: ${{ github.event_name }} on ${{ github.ref }} | |
| **Commit**: [${{ github.sha }}](${{ github.server_url }}/${{ github.repository }}/commit/${{ github.sha }}) | |
| **Details**: [Build log](${{ github.server_url }}/${{ github.repository }}/commit/${{ github.sha }}/checks) |