From 27760d4d31c13bcb82e4dec59925a5b2d56c6ebb 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 exynos5 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 | 57 ++++++++----------------------
 .github/workflows/proof.yml        | 12 +++----
 2 files changed, 18 insertions(+), 51 deletions(-)

diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml
index bf2006f651..0e7e86dba8 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 Exynos 5
 
 on:
   push:
     branches:
-      - master
-  repository_dispatch:
-    types:
-      - manifest-update
+      - exynos5-ver-rebased
   # for testing:
   workflow_dispatch:
 
@@ -36,14 +33,16 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
+        arch: [ARM_HYP]
+        plat: [exynos5]
     # 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 }}
       env:
         AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
@@ -61,47 +60,19 @@ jobs:
         name: logs-${{ 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 }}"
-
-  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@v3
       with:
-        ref: ${{ matrix.branch }}
-        path: l4v-${{ matrix.branch }}
+        ref: exynos5-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:exynos5-ver
diff --git a/.github/workflows/proof.yml b/.github/workflows/proof.yml
index 329394868b..df00bf3daa 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:
@@ -27,14 +21,16 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
-    # test only most recent push to PR:
+        arch: [ARM_HYP]
+        plat: [exynos5]
+    # 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 }}
         session: '-x AutoCorresSEL4' # exclude large AutoCorresSEL4 session for PRs
       env:
         AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}