chore: less Mac CI

Mac runners are a bottleneck, and are mostly there to check the subprocess interactions and installers. Remove some!
leanprover · Apr 19, 2024 · 02da67e · 02da67e
1 parent e8a85b2
commit 02da67e
Showing 1 changed file with 18 additions and 6 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -19,12 +19,24 @@ jobs:
           - os: ubuntu-latest
             installer: |
               curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-          - os: macos-latest
-            installer: |
-              curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-          - os: macos-latest
-            installer: |
-              brew install elan-init
+        # Mac runners are rare and expensive, so spot-check that the
+        # subprocess support seems OK but be less thorough
+        include:
+          - toolchain: "4.7.0"
+            platform:
+              os: macos-latest
+              installer: |
+                curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          - toolchain: "4.7.0"
+            platform:
+              os: macos-latest
+              installer: |
+                brew install elan-init
+          - toolchain: "4.3.0"
+            platform:
+              os: macos-latest
+              installer: |
+                brew install elan-init
     name: Build and test (${{ matrix.platform.os }}, ${{ matrix.platform.installer}}, ${{ matrix.toolchain}})
     runs-on: ${{ matrix.platform.os }}
     steps: