From 328d8fbf983feb02996688ae3f57abb9c21c2741 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 19 Apr 2024 15:32:30 +0200
Subject: [PATCH] chore: add Mac and homebrew to CI

---
 .github/workflows/ci.yml | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2101424..d51b50e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -15,14 +15,23 @@ jobs:
           - "leanprover/lean4:4.6.0"
           - "leanprover/lean4:4.7.0"
           - "leanprover/lean4: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
+          - 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
     name: Build and test
-    runs-on: ubuntu-latest
+    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?
@@ -56,8 +65,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