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 <[email protected]>

.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,38 +26,18 @@ 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
     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
+        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 "[email protected]"
+        git status
+        git push -f origin HEAD:imx8-fpu-ver

.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