From ff9d5eb11e03c9b38bbb38e2f103fd62302f0991 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Mon, 30 Oct 2023 16:29:51 -0400
Subject: [PATCH] Run regression tests on Apple Silicon runners, only on
 changes to `main` (#2845)

Adds a new workflow "Kani CI M1" that runs the regression suite on Apple
M1 runners (`macos-13-xlarge`), but only on pushes to `main`.

### Callouts
* Hasn't been tested since I don't have access to the `macos-13-xlarge`
runners in my fork.
* Added a new workflow to avoid making the "Kani CI" workflow more
complex. In particular, I first considered adding conditions to the
steps, but that would result in M1 runners being invoked only to skip
the job on PRs. Second, I tried adding a condition for the job itself,
but it's not possible to refer to `${{ os.matrix }}` at that stage.
* Similarly, I don't remove the `-xlarge` substring used for M1 runners.
---
 .github/workflows/kani-m1.yml | 30 ++++++++++++++++++++++++++++++
 scripts/setup/macos-13-xlarge |  1 +
 2 files changed, 31 insertions(+)
 create mode 100644 .github/workflows/kani-m1.yml
 create mode 120000 scripts/setup/macos-13-xlarge

diff --git a/.github/workflows/kani-m1.yml b/.github/workflows/kani-m1.yml
new file mode 100644
index 000000000000..e9f973c82919
--- /dev/null
+++ b/.github/workflows/kani-m1.yml
@@ -0,0 +1,30 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Run the regression job on Apple M1 only on commits to `main`
+name: Kani CI M1
+on:
+  push:
+    branches:
+      - 'main'
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  regression:
+    runs-on: macos-13-xlarge
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: macos-13-xlarge
+
+      - name: Build Kani
+        run: cargo build-dev
+
+      - name: Execute Kani regression
+        run: ./scripts/kani-regression.sh
diff --git a/scripts/setup/macos-13-xlarge b/scripts/setup/macos-13-xlarge
new file mode 120000
index 000000000000..a8d0f9c4854d
--- /dev/null
+++ b/scripts/setup/macos-13-xlarge
@@ -0,0 +1 @@
+macos
\ No newline at end of file