From d7f93db98b710cee24d84f5985e63451141dc856 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
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 <gerwin.klein@proofcraft.systems>
---
 .github/workflows/proof-deploy.yml | 65 +++++++-----------------------
 .github/workflows/proof.yml        | 12 ++----
 2 files changed, 18 insertions(+), 59 deletions(-)

diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml
index 7dcfad6b55..eb985ac095 100644
--- a/.github/workflows/proof-deploy.yml
+++ b/.github/workflows/proof-deploy.yml
@@ -1,18 +1,15 @@
-# 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
-  repository_dispatch:
-    types:
-      - manifest-update
+      - imx8-fpu-ver-rebased
   # for testing:
   workflow_dispatch:
 
@@ -36,15 +33,16 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
-        num_domains: ['1', '']
+        arch: [ARM]
+        plat: [imx8mm]
     # 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
       with:
         L4V_ARCH: ${{ matrix.arch }}
+        L4V_PLAT: ${{ matrix.plat }}
         xml: ${{ needs.code.outputs.xml }}
         NUM_DOMAINS: ${{ matrix.num_domains }}
       env:
@@ -63,54 +61,19 @@ jobs:
         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
+  push:
+    name: Push rebased branch
     runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        branch: [imx8-fpu-ver, exynos5-ver]
+    needs: [proofs]
     steps:
     - name: Checkout
       uses: actions/checkout@v4
       with:
-        ref: ${{ matrix.branch }}
-        path: l4v-${{ matrix.branch }}
+        ref: imx8-fpu-ver-rebased
         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
+    - name: Push
       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
+        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