Update push.yml

.github/workflows/push.yml

@@ -14,6 +14,7 @@ jobs:
     name: Lint style
     runs-on: ubuntu-latest
     steps:
+      # Check for long lines in .lean files and report if any lines exceed 100 characters
       - name: Check for long lines
         if: always()
         run: |
@@ -29,27 +30,24 @@ jobs:
     name: Build project
     steps:
       - name: Checkout project
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 
       - name: Install elan
         run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.7.0 #4.5.0
 
-      - name: Update docgen4
-        run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
-
-      - name: Update checkdecls
-        run: ~/.elan/bin/lake update checkdecls
+      # - name: Update doc-gen4
+      #   run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
 
       - name: Get cache
-        run: ~/.elan/bin/lake -R -Kenv=dev exe cache get || true
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
 
       - name: Build project
-        run: ~/.elan/bin/lake -R -Kenv=dev build FLT3
+        run: ~/.elan/bin/lake -Kenv=dev build FLT3
 
-      - name: Cache mathlib docs
-        uses: actions/cache@v3
+      - name: Cache mathlib documentation
+        uses: actions/cache@v4
         with:
           path: |
             .lake/build/doc/Init
@@ -58,19 +56,21 @@ jobs:
             .lake/build/doc/Std
             .lake/build/doc/Mathlib
             .lake/build/doc/declarations
+            .lake/build/doc/find
+            .lake/build/doc/*.*
             !.lake/build/doc/declarations/declaration-data-FLT3*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            MathlibDoc-
+          restore-keys: MathlibDoc-
 
-      - name: Build documentation
-        run: ~/.elan/bin/lake -R -Kenv=dev build FLT3:docs
+      - name: Build project documentation
+        run: ~/.elan/bin/lake -Kenv=dev build FLT3:docs
 
       - name: Build blueprint and copy to `docs/blueprint`
         uses: xu-cheng/texlive-action@v2
         with:
           docker_image: ghcr.io/xu-cheng/texlive-full:20231201
-          run: | # "mkdir docs" before "cp blueprint/print/print.pdf docs/blueprint.pdf"
+          run: |
+            export PIP_BREAK_SYSTEM_PACKAGES=1
             apk update
             apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
             git config --global --add safe.directory $GITHUB_WORKSPACE
@@ -86,34 +86,42 @@ jobs:
             cp -r blueprint/web docs/blueprint
 
       - name: Check declarations
-        run: |
-            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+        run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
-      - name: Move documentation to `docs/docs`
+      - name: Copy documentation to `docs/docs`
         run: |
           sudo chown -R runner docs
           cp -r .lake/build/doc docs/docs
 
+      - name: Remove lake files from documentation in `docs/docs`
+        run: |
+          find docs/docs -name "*.trace" -delete
+          find docs/docs -name "*.hash" -delete
+
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
         with:
           working-directory: docs
-          ruby-version: "3.0" # Not needed with a .ruby-version file
-          bundler-cache: true # runs 'bundle install' and caches installed gems automatically
+          ruby-version: "3.0"
+          bundler-cache: true
 
       - name: Bundle website
         working-directory: docs
         run: JEKYLL_ENV=production bundle exec jekyll build
 
-      - name: Upload docs & blueprint artifact
-        uses: actions/upload-pages-artifact@v1
+      # - name: Upload docs & blueprint artifact to `docs/`
+      #   uses: actions/upload-pages-artifact@v3
+      #   with:
+      #     path: docs/
+
+      - name: Upload docs & blueprint artifact to `docs/_site`
+        uses: actions/upload-pages-artifact@v3
         with:
           path: docs/_site
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v4
 
-      - name: Make sure the cache works
-        run: |
-          mv docs/docs .lake/build/doc
+      # - name: Make sure the cache works
+      #   run: mv docs/docs .lake/build/doc