chore: add Mac and homebrew to CI

leanprover · Apr 19, 2024 · 328d8fb · 328d8fb
1 parent 3d2c5f2
commit 328d8fb
Showing 1 changed file with 14 additions and 5 deletions.
diff --git 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