38e889da3b
Deploy the MCS verification manifest for versions that have no MCS preprocess differences. These may be different from non-MCS preprocess outcomes, and since the MCS verification is on a branch, we can deploy it separately. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
79 lines
1.8 KiB
YAML
79 lines
1.8 KiB
YAML
# Copyright 2021, Proofcraft Pty ltd
|
|
#
|
|
# SPDX-License-Identifier: BSD-2-Clause
|
|
|
|
# Sync proofs: deploy new verification manifest on successful preprocess test
|
|
|
|
name: Proof Sync
|
|
|
|
on:
|
|
push:
|
|
branches:
|
|
- master
|
|
workflow_dispatch:
|
|
|
|
jobs:
|
|
code:
|
|
name: Code Freeze
|
|
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
|
|
|
|
preprocess:
|
|
name: Preprocess
|
|
needs: code
|
|
runs-on: ubuntu-latest
|
|
strategy:
|
|
matrix:
|
|
arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
|
|
# no MCS here, see separate preprocess-mcs.
|
|
steps:
|
|
- uses: seL4/ci-actions/preprocess@master
|
|
with:
|
|
L4V_ARCH: ${{ matrix.arch }}
|
|
|
|
preprocess-mcs:
|
|
name: Preprocess (MCS)
|
|
needs: code
|
|
runs-on: ubuntu-latest
|
|
strategy:
|
|
matrix:
|
|
arch: [RISCV64]
|
|
steps:
|
|
- uses: seL4/ci-actions/preprocess@master
|
|
with:
|
|
L4V_ARCH: ${{ matrix.arch }}
|
|
L4V_FEATURES: "MCS"
|
|
|
|
deploy:
|
|
name: Deploy manifest
|
|
needs: [code, preprocess]
|
|
if: ${{ github.repository_owner == 'seL4' }}
|
|
runs-on: ubuntu-22.04
|
|
steps:
|
|
- uses: seL4/ci-actions/l4v-deploy@master
|
|
with:
|
|
xml: ${{ needs.code.outputs.xml }}
|
|
preprocess: 'true'
|
|
env:
|
|
GH_SSH: ${{ secrets.CI_SSH }}
|
|
|
|
deploy-mcs:
|
|
name: Deploy MCS manifest
|
|
needs: [code, preprocess-mcs]
|
|
if: ${{ github.repository_owner == 'seL4' }}
|
|
runs-on: ubuntu-22.04
|
|
steps:
|
|
- uses: seL4/ci-actions/l4v-deploy@master
|
|
with:
|
|
xml: ${{ needs.code.outputs.xml }}
|
|
preprocess: 'true'
|
|
manifest: mcs-devel.xml
|
|
env:
|
|
GH_SSH: ${{ secrets.CI_SSH }}
|