Skip to content

manifest-update

manifest-update #988

Workflow file for this run

# Copyright 2021 Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
# On push to master only: run proofs and deploy manifest update.
name: Proofs
on:
push:
branches:
- master
- rt
repository_dispatch:
types:
- manifest-update
# for testing:
workflow_dispatch:
jobs:
code:
name: Freeze Code
if: github.ref == 'refs/heads/master'
runs-on: ubuntu-latest
outputs:
xml: ${{ steps.repo.outputs.xml }}
steps:
- id: repo
uses: seL4/ci-actions/repo-checkout@master
with:
manifest_repo: verification-manifest
manifest: devel.xml
mcs-code:
name: Freeze MCS Code
if: github.ref == 'refs/heads/rt'
runs-on: ubuntu-latest
outputs:
xml: ${{ steps.repo.outputs.xml }}
steps:
- id: repo
uses: seL4/ci-actions/repo-checkout@master
with:
manifest_repo: verification-manifest
manifest: mcs-devel.xml
proofs:
name: Proof
needs: code
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
num_domains: ['1', '']
plat: ['']
include:
- arch: ARM_HYP
plat: exynos5
- arch: AARCH64
plat: zynqmp
- arch: AARCH64
plat: bcm2711
# test only most recent push:
concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }}
steps:
- name: Proofs
uses: seL4/ci-actions/aws-proofs@master
with:
L4V_ARCH: ${{ matrix.arch }}
L4V_PLAT: ${{ matrix.plat }}
xml: ${{ needs.code.outputs.xml }}
NUM_DOMAINS: ${{ matrix.num_domains }}
env:
AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
AWS_SSH: ${{ secrets.AWS_SSH }}
- name: Upload kernel builds
uses: actions/upload-artifact@v4
with:
name: kernel-builds-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }}
path: artifacts/kernel-builds
if-no-files-found: ignore
- name: Upload logs
uses: actions/upload-artifact@v4
with:
name: logs-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }}
path: logs.tar.xz
mcs-proofs:
name: MCS Proof
needs: mcs-code
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
arch: [ARM, RISCV64]
num_domains: ['1', '']
plat: [""]
# test only most recent push:
concurrency: l4v-mcs-regression-${{ github.ref }}-${{ strategy.job-index }}
steps:
- name: Proofs
uses: seL4/ci-actions/aws-proofs@master
with:
L4V_ARCH: ${{ matrix.arch }}
L4V_PLAT: ${{ matrix.plat }}
L4V_FEATURES: MCS
xml: ${{ needs.mcs-code.outputs.xml }}
NUM_DOMAINS: ${{ matrix.num_domains }}
env:
AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
AWS_SSH: ${{ secrets.AWS_SSH }}
- name: Upload kernel builds
uses: actions/upload-artifact@v4
with:
name: mcs-kernel-builds-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }}
path: artifacts/kernel-builds
if-no-files-found: ignore
- name: Upload logs
uses: actions/upload-artifact@v4
with:
name: mcs-logs-${{ matrix.num_domains }}-${{ matrix.arch }}-${{ matrix.plat }}
path: logs.tar.xz
deploy:
name: Deploy manifest
runs-on: ubuntu-latest
needs: [code, proofs]
steps:
- uses: seL4/ci-actions/l4v-deploy@master
with:
xml: ${{ needs.code.outputs.xml }}
env:
GH_SSH: ${{ secrets.CI_SSH }}
- name: Trigger binary verification
uses: seL4/ci-actions/bv-trigger@master
with:
token: ${{ secrets.PRIV_REPO_TOKEN }}
tag: "l4v/proof-deploy/${{ github.event_name }}"
mcs-deploy:
name: Deploy MCS manifest
runs-on: ubuntu-latest
needs: [mcs-code, mcs-proofs]
steps:
- uses: seL4/ci-actions/l4v-deploy@master
with:
xml: ${{ needs.mcs-code.outputs.xml }}
manifest: mcs-devel.xml
env:
GH_SSH: ${{ secrets.CI_SSH }}
# Automatically rebase platform branches on pushes to master.
trigger-rebase:
name: Trigger platform branch rebase
if: github.ref == 'refs/heads/master'
runs-on: ubuntu-latest
steps:
- name: Trigger rebase
uses: peter-evans/repository-dispatch@v3
with:
event-type: rebase