feat: use lean-action to install elan and lake build (#218)

* feat: use lean-action to install elan and `lake build` * doc: improve step name
leanprover · Sep 4, 2024 · 1b0072f · 1b0072f
1 parent 09aca1c
commit 1b0072f
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -14,12 +14,8 @@ jobs:
       - name: Checkout repo
         uses: actions/checkout@v4
 
-      - 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
+      - name: install elan and build doc-gen4
+        uses: leanprover/lean-action@v1
 
       - name: Checkout batteries
         run: |