consolidate builds #4836
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 | ||
|
Check failure on line 1 in .github/workflows/ci.yml
|
||
| on: | ||
| push: | ||
| branches: | ||
| - 'main' | ||
| - 'release' | ||
| - 'latest' | ||
| tags: | ||
| - 'r[0-9]+.[0-9]+' | ||
| pull_request: | ||
| merge_group: | ||
| env: | ||
| 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:${{ env.IMAGE_TAG }} | ||
| 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 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 | ||
| # ── Phase 3: Test in test box (no rebuild) ── | ||
| check: | ||
| name: Check EasyCrypt Libraries | ||
| needs: docker | ||
| runs-on: ubuntu-24.04 | ||
| container: | ||
| image: ghcr.io/easycrypt/ec-test-box:${{ env.IMAGE_TAG }} | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| target: [unit, stdlib, examples] | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| - name: Detect SMT provers | ||
| run: | | ||
| 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() | ||
| 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, fetch-external-matrix] | ||
| runs-on: ubuntu-24.04 | ||
| container: | ||
| image: ghcr.io/easycrypt/ec-test-box:${{ env.IMAGE_TAG }} | ||
| 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 | ||
| run: echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT | ||
| id: extract_branch | ||
| - 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 }} | ||
| - 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: | | ||
| 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 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:${{ env.IMAGE_TAG }} | ||
| docker tag ghcr.io/easycrypt/ec-base-box:${{ env.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:${{ env.IMAGE_TAG }} | ||
| docker tag ghcr.io/easycrypt/ec-build-box:${{ env.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:${{ env.IMAGE_TAG }} | ||
| docker tag ghcr.io/easycrypt/ec-test-box:${{ env.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] | ||
| 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) | ||
