More refactoring #2777
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,pull_request] | |
| env: | |
| HOME: /home/charlie | |
| OPAMYES: true | |
| OPAMJOBS: 2 | |
| jobs: | |
| pre_job: | |
| name: Check for Duplicates Jobs | |
| runs-on: ubuntu-20.04 | |
| outputs: | |
| should_skip: ${{ steps.skip_check.outputs.should_skip }} | |
| steps: | |
| - uses: fkirc/skip-duplicate-actions@v5 | |
| id: skip_check | |
| with: | |
| concurrent_skipping: 'same_content_newer' | |
| skip_after_successful_duplicate: 'false' | |
| compile-opam: | |
| name: EasyCrypt compilation (opam) | |
| needs: pre_job | |
| if: needs.pre_job.outputs.should_skip != 'true' | |
| runs-on: ubuntu-20.04 | |
| container: | |
| image: ghcr.io/easycrypt/ec-build-box | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Update OPAM & EasyCrypt dependencies | |
| run: | | |
| opam update | |
| opam pin add -n easycrypt . | |
| opam install --deps-only easycrypt | |
| - name: Compile EasyCrypt | |
| run: opam config exec -- make | |
| compile-nix: | |
| name: EasyCrypt compilation (nix) | |
| needs: pre_job | |
| if: needs.pre_job.outputs.should_skip != 'true' | |
| env: | |
| HOME: /home/runner | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Setup Nix | |
| uses: cachix/install-nix-action@v20 | |
| with: | |
| nix_path: nixpkgs=channel:nixos-unstable | |
| - name: Setup Cachix | |
| uses: cachix/cachix-action@v12 | |
| with: | |
| name: formosa-crypto | |
| authToken: '${{ secrets.CACHIX_WRITE_TOKEN }}' | |
| - name: Build and cache EasyCrypt and dependencies | |
| run: | | |
| nix-build | |
| check: | |
| name: Check EasyCrypt Libraries | |
| needs: [pre_job, compile-opam] | |
| if: needs.pre_job.outputs.should_skip != 'true' | |
| 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@v3 | |
| - name: Update OPAM & EasyCrypt dependencies | |
| run: | | |
| opam update | |
| opam pin add -n easycrypt . | |
| opam install --deps-only easycrypt | |
| - name: Compile EasyCrypt | |
| run: opam config exec -- make | |
| - name: Detect SMT provers | |
| run: | | |
| rm -f ~/.why3.conf | |
| opam config exec -- ./ec.native why3config -why3 ~/.why3.conf | |
| - name: Compile Library (${{ matrix.target }}) | |
| env: | |
| TARGET: ${{ matrix.target }} | |
| run: opam config exec -- make $TARGET | |
| - uses: actions/upload-artifact@v3 | |
| name: Upload report.log | |
| if: always() | |
| with: | |
| name: report.log (${{ matrix.target }}) | |
| path: report.log | |
| if-no-files-found: ignore | |
| external: | |
| name: Check EasyCrypt External Projects | |
| needs: [pre_job, compile-opam] | |
| if: needs.pre_job.outputs.should_skip != 'true' | |
| runs-on: ubuntu-20.04 | |
| container: | |
| image: ghcr.io/easycrypt/ec-build-box | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| target: [ [ 'jasmin-eclib', 'jasmin-lang/jasmin', 'eclib', 'tests.config', 'jasmin', '-p Z3@4.8 -p Alt-Ergo@2.4' ] ] | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| path: 'easycrypt' | |
| - uses: actions/checkout@v3 | |
| with: | |
| path: 'project' | |
| repository: ${{ matrix.target[1] }} | |
| - name: Update OPAM & EasyCrypt dependencies | |
| run: | | |
| opam update | |
| opam pin add -n easycrypt easycrypt | |
| opam install --deps-only easycrypt | |
| - name: Compile & Install EasyCrypt | |
| run: opam config exec -- make -C easycrypt build install | |
| - name: Detect SMT provers | |
| run: | | |
| rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf | |
| opam config exec -- easycrypt why3config | |
| - name: Compile project | |
| working-directory: project/${{ matrix.target[2] }} | |
| run: opam config exec -- ec-runtest ${{ matrix.target[5] }} ${{ matrix.target[3] }} ${{ matrix.target[4] }} | |
| - uses: actions/upload-artifact@v3 | |
| name: Upload report.log | |
| if: always() | |
| with: | |
| name: report.log (${{ matrix.target[0] }}) | |
| path: report.log | |
| if-no-files-found: ignore | |
| notification: | |
| name: Notification | |
| needs: [compile-opam, compile-nix, check, external] | |
| 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) |