This file contains 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 compilation & check | |
| on: | |
| push: | |
| branches: | |
| - 'main' | |
| pull_request: | |
| env: | |
| HOME: /home/charlie | |
| OPAMYES: true | |
| OPAMJOBS: 2 | |
| jobs: | |
| compile-opam: | |
| name: EasyCrypt compilation (opam) | |
| runs-on: ubuntu-20.04 | |
| container: | |
| image: ghcr.io/easycrypt/ec-build-box | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install EasyCrypt dependencies | |
| run: | | |
| opam pin add -n 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-20.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: compile-opam | |
| runs-on: ubuntu-20.04 | |
| container: | |
| image: ghcr.io/easycrypt/ec-build-box | |
| 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 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 | |
| - name: Compile Library (${{ matrix.target }}) | |
| env: | |
| TARGET: ${{ matrix.target }} | |
| run: 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-20.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: [compile-opam, fetch-external-matrix] | |
| runs-on: ubuntu-20.04 | |
| container: | |
| image: ghcr.io/easycrypt/ec-build-box | |
| 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: Install EasyCrypt dependencies | |
| run: | | |
| opam pin add -n easycrypt 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 }} | |
| 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-20.04 | |
| steps: | |
| - uses: re-actors/alls-green@release/v1 | |
| with: | |
| jobs: ${{ toJSON(needs) }} | |
| allowed-skips: external | |
| 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-20.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) |