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

.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,15 +33,16 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
-        num_domains: ['1', '']
+        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 }}
         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@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 "[email protected]"
-        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

.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 }}