chore: add Mac and homebrew to CI (#15)

leanprover · Apr 19, 2024 · b7e2e2d · b7e2e2d
1 parent 60b5dbc
commit b7e2e2d
Showing 1 changed file with 35 additions and 14 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -2,27 +2,48 @@ on:
   push:
   pull_request:
 
-name: Continuous Integration
+name: CI
 
 jobs:
   build:
     strategy:
       matrix:
         toolchain:
-          - "leanprover/lean4:4.3.0"
-          - "leanprover/lean4:4.4.0"
-          - "leanprover/lean4:4.5.0"
-          - "leanprover/lean4:4.6.0"
-          - "leanprover/lean4:4.7.0"
-          - "leanprover/lean4:nightly-2024-04-07"
-    name: Build and test
-    runs-on: ubuntu-latest
+          - "4.3.0"
+          - "4.4.0"
+          - "4.5.0"
+          - "4.6.0"
+          - "4.7.0"
+          - "nightly-2024-04-07"
+        platform:
+          - os: ubuntu-latest
+            installer: |
+              curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+        # 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:
       - name: Install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
+          ${{ matrix.platform.installer }}
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: Which lake?
@@ -37,7 +58,7 @@ jobs:
 
       - name: Select Lean version
         run: |
-          echo "${{ matrix.toolchain }}" > lean-toolchain
+          echo "leanprover/lean4:${{ matrix.toolchain }}" > lean-toolchain
 
       - name: Lean version
         run: |
@@ -56,8 +77,8 @@ jobs:
       - name: Configure demo/test subproject
         run: |
           pushd demo
-          ~/.elan/bin/lake update
-          ~/.elan/bin/lake build :examples
+          lake update
+          lake build :examples
           popd
 
       - name: Run tests