Fix disk space issue (#32)

.github/workflows/push.yml

@@ -23,25 +23,24 @@ jobs:
     runs-on: ubuntu-latest
     name: Build project
     steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
       - name: Checkout project
         uses: actions/checkout@v2
         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.0.0
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 # Install Lean 4
+
+      - name: Update docgen4
+        run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
 
       - name: Get cache
         run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
 
       - name: Build project
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis
 
-
       - name: Cache mathlib docs
         uses: actions/cache@v3
         with:
@@ -55,56 +54,55 @@ jobs:
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
-            MathlibDoc-
+            MathlibDoc- # Cache Mathlib documentation to save rebuild time
 
-
-      # - name: Build documentation
-      #   run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
 
       - name: Install Python
         uses: actions/setup-python@v4
         with:
           python-version: '3.9'
-          cache: 'pip' # caching pip dependencies
+          cache: 'pip'
 
       - name: Install blueprint apt dependencies
         run: |
           sudo apt-get update
-          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
 
       - name: Install blueprint dependencies
         run: |
-          cd blueprint && pip install -r requirements.txt
+          cd blueprint && pip install -r requirements.txt # Install Python dependencies for blueprint
 
       - name: Build blueprint and copy to `docs/blueprint`
+        run: inv all
+
+      - name: Remove lake files from documentation
         run: |
-          inv all
+          find .lake/build/doc -name "*.trace" -delete
+          find .lake/build/doc -name "*.hash" -delete
 
-      # - name: Copy documentation to `docs/docs`
-      #   run: |
-      #     sudo chown -R runner docs
-      #     cp -r .lake/build/doc docs/docs
+      - name: Copy documentation to `docs/docs`
+        run: |
+          sudo chown -R runner docs
+          cp -r .lake/build/doc docs/docs # Copy the built documentation to the correct directory
 
-      # - 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
+      - name: Bundle dependencies
+        uses: ruby/setup-ruby@v1
+        with:
+          working-directory: docs
+          ruby-version: "3.0"
+          bundler-cache: true
 
-      # - name: Bundle website
-      #   working-directory: docs
-      #   run: JEKYLL_ENV=production bundle exec jekyll build
+      - name: Bundle website
+        working-directory: docs
+        run: JEKYLL_ENV=production bundle exec jekyll build # Build the Jekyll site for production
 
       - name: Upload docs & blueprint artifact
         uses: actions/upload-pages-artifact@v1
         with:
-          path: docs/
+          path: docs/_site
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
-
-      #  - name: Make sure the cache works
-      #    run: |
-          #  mv docs/docs .lake/build/doc
+        uses: actions/deploy-pages@v1