From 7c765b5edbea540de20e2efdeecdd02023ed5c77 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <ahelwer@pm.me>
Date: Mon, 20 Apr 2026 09:20:12 -0700
Subject: [PATCH] CI: run proof checks on push to master

Signed-off-by: Andrew Helwer <ahelwer@pm.me>
---
 .github/workflows/CI.yml     | 14 -----------
 .github/workflows/proofs.yml | 46 ++++++++++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 14 deletions(-)
 create mode 100644 .github/workflows/proofs.yml

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index cf626601..21abb0a3 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -132,20 +132,6 @@ jobs:
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --examples_root .                                            \
             --skip "${SKIP[@]}"
-      - name: Check proofs
-        if: matrix.os != 'windows-latest' && !matrix.unicode
-        run: |
-          set -o pipefail
-          find specifications -iname "manifest.json" -print0 \
-          | xargs --null --no-run-if-empty \
-          jq --join-output '
-            .modules
-            | map(select(has("proof")))
-            | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
-            | map(.path + "\u0000")
-            | join("")' \
-          | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
-          "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \
diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
new file mode 100644
index 00000000..5022bb53
--- /dev/null
+++ b/.github/workflows/proofs.yml
@@ -0,0 +1,46 @@
+name: Check Proofs
+on:
+  push:
+    branches:
+      - master
+concurrency:
+  group: ${{ github.workflow }}
+  cancel-in-progress: true
+
+jobs:
+  check:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+      fail-fast: false
+    env:
+      SCRIPT_DIR: .github/scripts
+      DEPS_DIR: deps
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - name: Clone repo
+        uses: actions/checkout@v4
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+      - name: Install dependencies
+        run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false
+      - name: Check proofs
+        run: |
+          set -o pipefail
+          find specifications -iname "manifest.json" -print0 \
+          | xargs --null --no-run-if-empty \
+          jq --join-output '
+            .modules
+            | map(select(has("proof")))
+            # Failing on Linux
+            | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
+            | map(.path + "\u0000")
+            | join("")' \
+          | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
+          time "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
+