refactor: use lean-action in makefile.yml CI workflow (#102)

### Description: `lean-action` now supports the macOS runner so you can now use it in makefile.yml ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Closes #82 --------- Co-authored-by: Shilpi Goel <[email protected]>
leanprover · Aug 21, 2024 · 4fec93c · 4fec93c
1 parent 5f90bf9
commit 4fec93c
Showing 1 changed file with 5 additions and 8 deletions.
diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml
@@ -27,14 +27,11 @@ jobs:
 
     - uses: actions/checkout@v4
 
-    # We would like to use `leanprover/lean-action`, but it doesn't work on macOS just yet:
-    #   https://github.com/leanprover/lean-action/issues/83
-    - name: Install elan
-      run: |
-        set -o pipefail
-        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
-        ~/.elan/bin/lean --version
-        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+    - uses: leanprover/lean-action@v1
+      with:
+        auto-config: false
+        use-mathlib-cache: false
+        use-github-cache: true
 
     - name: Cache `.lake` folder
       id: cache-lake