Skip to content

docs: document platform branch procedure #912

docs: document platform branch procedure

docs: document platform branch procedure #912

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
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@v4
with:
name: kernel-builds-${{ matrix.num_domains }}-${{ matrix.arch }}
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 }}
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@v4
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 "[email protected]"
git rebase origin/master
git status
- name: Push
run: |
cd l4v-${{ matrix.branch }}
git push -f origin HEAD:${{ matrix.branch }}-rebased