117 lines
3.4 KiB
YAML
117 lines
3.4 KiB
YAML
# 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
|
|
repository_dispatch:
|
|
types:
|
|
- manifest-update
|
|
# for testing:
|
|
workflow_dispatch:
|
|
|
|
jobs:
|
|
code:
|
|
name: Freeze Code
|
|
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
|
|
|
|
proofs:
|
|
name: Proof
|
|
needs: code
|
|
runs-on: ubuntu-latest
|
|
strategy:
|
|
fail-fast: false
|
|
matrix:
|
|
arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
|
|
num_domains: ['1', '']
|
|
# 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 }}
|
|
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@v3
|
|
with:
|
|
name: kernel-builds
|
|
path: artifacts/kernel-builds
|
|
if-no-files-found: ignore
|
|
- name: Upload logs
|
|
uses: actions/upload-artifact@v3
|
|
with:
|
|
name: logs-${{ matrix.num_domains }}-${{ matrix.arch }}
|
|
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 }}"
|
|
|
|
# Automatically rebase platform branches on pushes to master.
|
|
# This workflow here on the master branch attempts a git rebase of the platform
|
|
# branches listed in the build matrix below. If the rebase succeeds, the rebased
|
|
# branch is pushed under the name `<branch>-rebased`. This triggers the build
|
|
# workflow on the `<branch>-rebased` branch, which will run the proofs. If the
|
|
# proofs succeed, the `<branch>-rebased` branch is force-pushed over
|
|
# `<branch>`, becoming the new platform branch.
|
|
rebase:
|
|
name: Rebase platform branches
|
|
runs-on: ubuntu-latest
|
|
strategy:
|
|
fail-fast: false
|
|
matrix:
|
|
branch: [imx8-fpu-ver, exynos5-ver]
|
|
steps:
|
|
- name: Checkout
|
|
uses: actions/checkout@v3
|
|
with:
|
|
ref: ${{ matrix.branch }}
|
|
path: l4v-${{ matrix.branch }}
|
|
fetch-depth: 0
|
|
# needed to trigger push actions on the -rebased branch
|
|
# (implict GITHUB_TOKEN does not trigger further push actions).
|
|
token: ${{ secrets.PRIV_REPO_TOKEN }}
|
|
- name: Rebase
|
|
run: |
|
|
cd l4v-${{ matrix.branch }}
|
|
git config --global user.name "seL4 CI"
|
|
git config --global user.email "ci@sel4.systems"
|
|
git rebase origin/master
|
|
git status
|
|
- name: Push
|
|
run: |
|
|
cd l4v-${{ matrix.branch }}
|
|
git push -f origin HEAD:${{ matrix.branch }}-rebased
|