1# Copyright 2021 Proofcraft Pty Ltd
2#
3# SPDX-License-Identifier: BSD-2-Clause
4
5name: Proofs
6
7on:
8  pull_request_target:
9    types: [labeled, synchronize]
10
11jobs:
12  cproof:
13    name: C Proofs
14    runs-on: ubuntu-latest
15    # run on any normal trigger when the label exists, and run when the label is added
16    # don't run again when other labels are added
17    if: ${{ github.repository_owner == 'seL4' &&
18            (github.event.action != 'labeled' &&
19               contains(github.event.pull_request.labels.*.name, 'proof-test') ||
20             github.event.action == 'labeled' && github.event.label.name == 'proof-test') }}
21    strategy:
22      fail-fast: false
23      matrix:
24        include:
25          - arch: ARM
26            session: CRefine SimplExportAndRefine
27          - arch: ARM_HYP
28            session: CRefine
29          - arch: RISCV64
30            session: CRefine SimplExportAndRefine
31          - arch: X64
32            session: CRefine
33    steps:
34    - name: Proofs
35      uses: seL4/ci-actions/aws-proofs@master
36      with:
37        L4V_ARCH: ${{ matrix.arch }}
38        isa_branch: ts-2021
39        session: ${{ matrix.session }}
40        manifest: default.xml
41      env:
42        AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
43        AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
44        AWS_SSH: ${{ secrets.AWS_SSH }}
45        GH_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
46    - name: Upload logs
47      uses: actions/upload-artifact@v2
48      with:
49        name: logs-${{ matrix.arch }}
50        path: logs.tar.xz
51