ci.yml

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)