Skip to content
EasyCrypt compilation & check

Simple tactics in proof-terms. #3125

Sign in to view logs

Simple tactics in proof-terms.

Simple tactics in proof-terms. #3125

Workflow file for this run

.github/workflows/ci.yml at 2d0e6cf
name: EasyCrypt compilation & check
on: [push,pull_request,merge_group]
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@v4
- name: Install EasyCrypt dependencies
run: |
opam pin add -n easycrypt .
opam install --deps-only easycrypt
- name: Compile EasyCrypt
run: opam 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@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: [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@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
needs: [pre_job]
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: [pre_job, compile-opam, fetch-external-matrix]
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: ${{fromJson(needs.fetch-external-matrix.outputs.matrix)}}
steps:
- uses: actions/checkout@v4
with:
path: easycrypt
- name: Checkout External Project
run: |
git clone --recurse-submodules \
-b ${{ matrix.target.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)