From dbab25c8d3c1d693d704b681c8ee660de10d38ba Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Wed, 18 Aug 2021 13:26:13 +1000
Subject: [PATCH] github: deploy verification-manifest on preprocess

Automatically keep verification-manifest in sync with
preprocess-equivalent changes.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 .github/workflows/preprocess-deploy.yml | 50 +++++++++++++++++++++++++
 README.md                               |  1 +
 2 files changed, 51 insertions(+)
 create mode 100644 .github/workflows/preprocess-deploy.yml

diff --git a/.github/workflows/preprocess-deploy.yml b/.github/workflows/preprocess-deploy.yml
new file mode 100644
index 000000000..d735fe075
--- /dev/null
+++ b/.github/workflows/preprocess-deploy.yml
@@ -0,0 +1,50 @@
+# Copyright 2021, Proofcraft Pty ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# Sync proofs: deploy new verification manifest on successful preprocess test
+
+name: Proof Sync
+
+on:
+  push:
+    branches:
+      - master
+
+jobs:
+  code:
+    name: Code Freeze
+    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: devel.xml
+
+  preprocess:
+    name: Preprocess
+    needs: code
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        arch: [ARM, ARM_HYP, RISCV64, X64]
+        # no MCS here, auto-updating mcs.xml should be a separate job.
+    steps:
+    - uses: seL4/ci-actions/preprocess@master
+      with:
+        L4V_ARCH: ${{ matrix.arch }}
+
+  deploy:
+    name: Deploy manifest
+    needs: [code, preprocess]
+    runs-on: ubuntu-latest
+    steps:
+    - uses: seL4/ci-actions/l4v-deploy@master
+      with:
+        xml: ${{ needs.code.outputs.xml }}
+        preprocess: 'true'
+      env:
+        GH_SSH: ${{ secrets.CI_SSH }}
diff --git a/README.md b/README.md
index e777f60cc..420e7c64d 100644
--- a/README.md
+++ b/README.md
@@ -12,6 +12,7 @@ The seL4 microkernel
 [![Simulation](https://github.com/seL4/seL4/actions/workflows/sel4test-sim.yml/badge.svg)](https://github.com/seL4/seL4/actions/workflows/sel4test-sim.yml)
 [![C Parser](https://github.com/seL4/seL4/actions/workflows/cparser.yml/badge.svg)](https://github.com/seL4/seL4/actions/workflows/cparser.yml)
 [![Kernel](https://github.com/seL4/seL4/actions/workflows/compilation-checks.yml/badge.svg)](https://github.com/seL4/seL4/actions/workflows/compilation-checks.yml)
+[![Proof Sync](https://github.com/seL4/seL4/actions/workflows/preprocess-deploy.yml/badge.svg)](https://github.com/seL4/seL4/actions/workflows/preprocess-deploy.yml)
 [![RefMan](https://github.com/seL4/seL4/actions/workflows/manual.yml/badge.svg)](https://github.com/seL4/seL4/actions/workflows/manual.yml)
 [![XML](https://github.com/seL4/seL4/actions/workflows/xml_lint.yml/badge.svg)](https://github.com/seL4/seL4/actions/workflows/xml_lint.yml)