Use lean-action in Lean CI job (#1319)

Use the official Lean GitHub action. This simplifies the workflow and
fixes the recent installation issue that has come up in CI for Lean.

Author: jordancarlin

.github/workflows/compile-lean.yml

@@ -30,37 +30,13 @@ jobs:
         with:
           sail-version: "latest"
 
-      - name: Install Lean
-        run: |
-          wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh
-          bash install_debian.sh ; rm -f install_debian.sh
-
       - name: Build the Sail RISCV Model for Lean
         run: |
           eval $(opam config env)
           cmake -S . -B build -DCMAKE_BUILD_TYPE=RelWithDebInfo -G Ninja
           cmake --build build/ --target generated_lean_rv64d generated_lean_executable_rv64d
 
-      - name: Restore cached .lake directory
-        id: cache-lake-restore
-        uses: actions/cache/restore@v4
-        with:
-          path: |
-            build/model/Lean_RV64D/.lake
-            build/model/Lean_RV64D_executable/.lake
-          key: ${{ matrix.os }}-lake
-
       - name: Use Lean to build the model and report errors
-        run: |
-          source ~/.profile
-          cd build/model/Lean_RV64D/
-          lake build
-
-      - name: Save cached .lake directory
-        id: cache-lake-save
-        uses: actions/cache/save@v4
+        uses: leanprover/lean-action@v1
         with:
-          path: |
-            build/model/Lean_RV64D/.lake
-            build/model/Lean_RV64D_executable/.lake
-          key: ${{ steps.cache-lake-restore.outputs.cache-primary-key }}
+          lake-package-directory: "build/model/Lean_RV64D/"