From 956e9ac4e3bfd540764a6c72689dfe504b583c63 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 5 Jun 2023 10:37:50 +1000 Subject: [PATCH] github: add imx8mm workflow for branch push Use the deployment action to push the rebased version of the branch after proofs complete successfully. Signed-off-by: Gerwin Klein --- .github/workflows/proof-deploy.yml | 126 +++++------------------------ .github/workflows/proof.yml | 12 +-- 2 files changed, 25 insertions(+), 113 deletions(-) diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml index 66ab7d2f44..bfdaa6084f 100644 --- a/.github/workflows/proof-deploy.yml +++ b/.github/workflows/proof-deploy.yml @@ -1,26 +1,21 @@ -# Copyright 2021 Proofcraft Pty Ltd +# Copyright 2023 Proofcraft Pty Ltd # # SPDX-License-Identifier: BSD-2-Clause -# On push to master only: run proofs and deploy manifest update. +# Run proofs and rebase plaform branch. -name: Proofs +name: Platform Proofs IMX8MM on: push: branches: - - master - - rt - repository_dispatch: - types: - - manifest-update + - imx8-fpu-ver-rebased # 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 }} @@ -31,19 +26,6 @@ jobs: 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 @@ -51,18 +33,11 @@ jobs: 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 + arch: [ARM] + plat: [imx8mm] + num_domains: [''] # test only most recent push: - concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }} + concurrency: l4v-${{ github.ref }}-${{ strategy.job-index }} steps: - name: Proofs uses: seL4/ci-actions/aws-proofs@master @@ -87,78 +62,19 @@ jobs: 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' + push: + name: Push rebased branch runs-on: ubuntu-latest + needs: [proofs] steps: - - name: Trigger rebase - uses: peter-evans/repository-dispatch@v3 + - name: Checkout + uses: actions/checkout@v4 with: - event-type: rebase + ref: imx8-fpu-ver-rebased + fetch-depth: 0 + - name: Push + run: | + git config --global user.name "seL4 CI" + git config --global user.email "ci@sel4.systems" + git status + git push -f origin HEAD:imx8-fpu-ver diff --git a/.github/workflows/proof.yml b/.github/workflows/proof.yml index 02bb6ce83a..e2762c3583 100644 --- a/.github/workflows/proof.yml +++ b/.github/workflows/proof.yml @@ -5,12 +5,6 @@ name: Proof PR on: - push: - paths-ignore: - - '**.md' - - '**.txt' - branches: - - rt # this action needs access to secrets. # The actual test runs in a no-privilege VM, so it's Ok to run on untrusted PRs. pull_request_target: @@ -31,14 +25,16 @@ jobs: strategy: fail-fast: false matrix: - arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] - # test only most recent push to PR: + arch: [ARM] + plat: [imx8mm] + # test only most recent push to PR or branch: concurrency: l4v-pr-${{ github.event.number }}-idx-${{ strategy.job-index }} steps: - name: Proofs uses: seL4/ci-actions/aws-proofs@master with: L4V_ARCH: ${{ matrix.arch }} + L4V_PLAT: ${{ matrix.plat }} NUM_DOMAINS: ${{ inputs.NUM_DOMAINS }} skip_dups: true session: '-x AutoCorresSEL4' # exclude large AutoCorresSEL4 session for PRs