try

Author: astrainfinita

.github/workflows/docs.yml

@@ -1,9 +1,9 @@
-name: Build docs
+name: build and deploy docs
 
 on:
   push:
     branches:
-      - "master"
+      - master
   pull_request:
 
 permissions:
@@ -13,29 +13,69 @@ permissions:
 
 jobs:
   build:
+    name: build and deploy docs
     runs-on: ubuntu-latest
     steps:
-      - name: Checkout Project
+      - name: clean up
+        run: |
+          rm -rf Algorithm
+          rm -rf $HOME/.elan
+          rm -rf $HOME/.cache/mathlib
+
+      - name: Checkout repo
         uses: actions/checkout@v4
         with:
           fetch-depth: 2
           lfs: true
-      - name: Install Lean
+
+      - name: install elan
         run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s - -y --default-toolchain `cat ./lean-toolchain`
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - run: |
-          lake -Kenv=CI_BUILD exe cache get && lake -Kenv=CI_BUILD build && lake -Kenv=CI_BUILD build Algorithm:docs
-      - name: Fix permissions
+
+      - name: set default toolchain
+        working-directory: Algorithm
+        run: |
+          elan default $(cat lean-toolchain)
+
+      - name: get cache
+        working-directory: Algorithm
+        run: lake exe cache get
+
+      - name: build algorithm
+        working-directory: Algorithm
+        run: env LEAN_ABORT_ON_PANIC=1 lake build
+
+      - name: build doc-gen4
+        working-directory: Algorithm
         run: |
-          chmod -c -R +rX "./.lake/build/doc/" | while read line; do
-            echo "::warning title=Invalid file permissions automatically fixed::$line"
-          done
+          lake build doc-gen4
+
+      - name: build import graph
+        working-directory: Algorithm
+        run: |
+          lake exe graph ./.lake/build/doc/algorithm.html
+
+      - name: generate docs
+        working-directory: workaround
+        run: |
+          lake build Algorithm:docs
+          lake build Algorithm:docsHeader
+
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v3
         with:
-          path: ./.lake/build/doc/
+          path: './.lake/build/doc'
+
       - name: Deploy to GitHub Pages
         if: github.ref == 'refs/heads/master'
         id: deployment
         uses: actions/deploy-pages@v4
+
+      - name: clean up
+        if: always()
+        run: |
+          rm -rf Algorithm
+          rm -rf $HOME/.elan
+          rm -rf $HOME/.cache/mathlib