From fcafdcfc862956a511ab20ee0170212c31bf23ea Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Fri, 26 Jul 2024 10:26:43 +1000
Subject: [PATCH] github: factor out platform rebase into own workflow

Factor out the platform branch rebase job into its own workflow which is
triggered explicitly by a repository-dispatch event.

We can then re-trigger the rebase job after the proofs have succeeded on
the rebased branch to confirm that everything is now up to date and get
a successful rebase test run after everything has completed.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/proof-deploy.yml | 38 ++++-------------------
 .github/workflows/rebase.yml       | 50 ++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+), 32 deletions(-)
 create mode 100644 .github/workflows/rebase.yml

diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml
index 74fdbf0ab4..66ab7d2f44 100644
--- a/.github/workflows/proof-deploy.yml
+++ b/.github/workflows/proof-deploy.yml
@@ -152,39 +152,13 @@ jobs:
       env:
         GH_SSH: ${{ secrets.CI_SSH }}
 
-# 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
+  # Automatically rebase platform branches on pushes to master.
+  trigger-rebase:
+    name: Trigger platform branch rebase
     if: github.ref == 'refs/heads/master'
     runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        branch: [imx8-fpu-ver]
     steps:
-    - name: Checkout
-      uses: actions/checkout@v4
+    - name: Trigger rebase
+      uses: peter-evans/repository-dispatch@v3
       with:
-        ref: ${{ matrix.branch }}
-        path: l4v-${{ matrix.branch }}
-        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
-      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
+        event-type: rebase
diff --git a/.github/workflows/rebase.yml b/.github/workflows/rebase.yml
new file mode 100644
index 0000000000..fbbbcc5536
--- /dev/null
+++ b/.github/workflows/rebase.yml
@@ -0,0 +1,50 @@
+# Copyright 2024 Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# On repository dispatch event rebase platform branches.
+
+name: Rebase
+
+on:
+  repository_dispatch:
+    types:
+      - rebase
+  # for testing:
+  workflow_dispatch:
+
+# 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.
+jobs:
+  rebase:
+    name: Rebase platform branches
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        branch: [imx8-fpu-ver]
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+      with:
+        ref: ${{ matrix.branch }}
+        path: l4v-${{ matrix.branch }}
+        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
+      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