From de5da0f4d85842dbc81a90f1e930ce248cead3d4 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 08:02:11 +0200
Subject: [PATCH 01/42] Update push.yml

---
 .github/workflows/push.yml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 6727a41..239f4a4 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -2,6 +2,7 @@ on:
   push:
     branches:
       - master
+      - gh-actions
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
@@ -70,6 +71,14 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
 
+      - name: Cache blueprint dependencies
+        uses: actions/cache@v3
+        with:
+          path: ~/.cache/pip
+          key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
+          restore-keys: |
+            blueprint-dependencies- # Cache Python dependencies for blueprint
+
       - name: Install blueprint dependencies
         run: |
           cd blueprint && pip install -r requirements.txt # Install Python dependencies for blueprint

From 9e340db1b0cf7d004ecd9c1c3d769a0e28f09a60 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 08:09:56 +0200
Subject: [PATCH 02/42] Update push.yml

---
 .github/workflows/push.yml | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 239f4a4..f07551f 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -58,7 +58,7 @@ jobs:
             MathlibDoc- # Cache Mathlib documentation to save rebuild time
 
       - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
+        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 
       - name: Install Python
         uses: actions/setup-python@v4
@@ -66,6 +66,22 @@ jobs:
           python-version: '3.9'
           cache: 'pip'
 
+      - name: Cache apt packages
+        uses: actions/cache@v3
+        with:
+          path: /var/cache/apt
+          key: apt-cache-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
+          restore-keys: |
+            apt-cache-${{ runner.os }}-
+
+      - name: Cache apt package lists
+        uses: actions/cache@v3
+        with:
+          path: /var/lib/apt/lists
+          key: apt-lists-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
+          restore-keys: |
+            apt-lists-${{ runner.os }}-
+
       - name: Install blueprint apt dependencies
         run: |
           sudo apt-get update
@@ -105,7 +121,7 @@ jobs:
 
       - name: Bundle website
         working-directory: docs
-        run: JEKYLL_ENV=production bundle exec jekyll build # Build the Jekyll site for production
+        run: JEKYLL_ENV=production bundle exec jekyll build
 
       - name: Upload docs & blueprint artifact
         uses: actions/upload-pages-artifact@v1

From 97ea6dfcbc686352d2b93f5b15770eda1cc21c32 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 08:11:58 +0200
Subject: [PATCH 03/42] Update push.yml

---
 .github/workflows/push.yml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index f07551f..658d85f 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -87,13 +87,13 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
 
-      - name: Cache blueprint dependencies
-        uses: actions/cache@v3
-        with:
-          path: ~/.cache/pip
-          key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
-          restore-keys: |
-            blueprint-dependencies- # Cache Python dependencies for blueprint
+      # - name: Cache blueprint dependencies
+      #   uses: actions/cache@v3
+      #   with:
+      #     path: ~/.cache/pip
+      #     key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
+      #     restore-keys: |
+      #       blueprint-dependencies- # Cache Python dependencies for blueprint
 
       - name: Install blueprint dependencies
         run: |

From baf36f94bd0bac61e0d0fa46168d99bcb57cd5f0 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 08:24:20 +0200
Subject: [PATCH 04/42] Update push.yml

---
 .github/workflows/push.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 658d85f..ed3ebf8 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -57,6 +57,14 @@ jobs:
           restore-keys: |
             MathlibDoc- # Cache Mathlib documentation to save rebuild time
 
+      - name: Cache documentation build artifacts
+        uses: actions/cache@v3
+        with:
+          path: .lake/build
+          key: build-artifacts-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            build-artifacts-
+
       - name: Build documentation
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 

From 80240b32dbeb8df437cbab65f5bf0acadec9d528 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 08:29:50 +0200
Subject: [PATCH 05/42] Update push.yml

---
 .github/workflows/push.yml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index ed3ebf8..2920636 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -66,7 +66,7 @@ jobs:
             build-artifacts-
 
       - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
+        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
 
       - name: Install Python
         uses: actions/setup-python@v4
@@ -95,13 +95,13 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
 
-      # - name: Cache blueprint dependencies
-      #   uses: actions/cache@v3
-      #   with:
-      #     path: ~/.cache/pip
-      #     key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
-      #     restore-keys: |
-      #       blueprint-dependencies- # Cache Python dependencies for blueprint
+      - name: Cache blueprint dependencies
+        uses: actions/cache@v3
+        with:
+          path: ~/.cache/pip
+          key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
+          restore-keys: |
+            blueprint-dependencies- # Cache Python dependencies for blueprint
 
       - name: Install blueprint dependencies
         run: |
@@ -129,7 +129,7 @@ jobs:
 
       - name: Bundle website
         working-directory: docs
-        run: JEKYLL_ENV=production bundle exec jekyll build
+        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

From 7fc59036984cc556782c66357fc5c9160bdba1fb Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 08:50:50 +0200
Subject: [PATCH 06/42] Exclude directories requiring special permissions

---
 .github/workflows/push.yml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 2920636..2c76062 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -61,7 +61,7 @@ jobs:
         uses: actions/cache@v3
         with:
           path: .lake/build
-          key: build-artifacts-${{ hashFiles('lake-manifest.json') }}
+          key: build-artifacts-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             build-artifacts-
 
@@ -77,7 +77,9 @@ jobs:
       - name: Cache apt packages
         uses: actions/cache@v3
         with:
-          path: /var/cache/apt
+          path: |
+            /var/cache/apt/archives
+            !/var/cache/apt/archives/partial
           key: apt-cache-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
           restore-keys: |
             apt-cache-${{ runner.os }}-
@@ -85,7 +87,10 @@ jobs:
       - name: Cache apt package lists
         uses: actions/cache@v3
         with:
-          path: /var/lib/apt/lists
+          path: |
+            /var/lib/apt/lists
+            !/var/lib/apt/lists/partial
+            !/var/lib/apt/lists/lock
           key: apt-lists-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
           restore-keys: |
             apt-lists-${{ runner.os }}-
@@ -99,7 +104,7 @@ jobs:
         uses: actions/cache@v3
         with:
           path: ~/.cache/pip
-          key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
+          key: blueprint-dependencies-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
           restore-keys: |
             blueprint-dependencies- # Cache Python dependencies for blueprint
 

From 42db13911f379c55478369d1e3079bf8ae4a0918 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 09:08:13 +0200
Subject: [PATCH 07/42] Update push.yml

---
 .github/workflows/push.yml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 2c76062..a1f15ae 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -57,13 +57,13 @@ jobs:
           restore-keys: |
             MathlibDoc- # Cache Mathlib documentation to save rebuild time
 
-      - name: Cache documentation build artifacts
-        uses: actions/cache@v3
-        with:
-          path: .lake/build
-          key: build-artifacts-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            build-artifacts-
+      # - name: Cache documentation build artifacts
+      #   uses: actions/cache@v3
+      #   with:
+      #     path: .lake/build
+      #     key: build-artifacts-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}
+      #     restore-keys: |
+      #       build-artifacts-
 
       - name: Build documentation
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation

From dedbc9e5bb6526a2f2c3c61a0234b1bde5015933 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 09:31:48 +0200
Subject: [PATCH 08/42] Update push.yml

---
 .github/workflows/push.yml | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index a1f15ae..61b7b96 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -57,14 +57,6 @@ jobs:
           restore-keys: |
             MathlibDoc- # Cache Mathlib documentation to save rebuild time
 
-      # - name: Cache documentation build artifacts
-      #   uses: actions/cache@v3
-      #   with:
-      #     path: .lake/build
-      #     key: build-artifacts-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}
-      #     restore-keys: |
-      #       build-artifacts-
-
       - name: Build documentation
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
 

From a5501920ebee5d5223bde80a288a9b0845c0ce7b Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 09:45:04 +0200
Subject: [PATCH 09/42] Update push.yml

---
 .github/workflows/push.yml | 48 +++++++++++++++++++-------------------
 1 file changed, 24 insertions(+), 24 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 61b7b96..e6e3894 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -67,38 +67,38 @@ jobs:
           cache: 'pip'
 
       - name: Cache apt packages
+        id: cache-apt
         uses: actions/cache@v3
         with:
-          path: |
-            /var/cache/apt/archives
-            !/var/cache/apt/archives/partial
-          key: apt-cache-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
+          path: ./cache/apt
+          key: apt-packages-${{ hashFiles('blueprint/requirements.txt') }}
           restore-keys: |
-            apt-cache-${{ runner.os }}-
+            apt-packages-
 
-      - name: Cache apt package lists
-        uses: actions/cache@v3
-        with:
-          path: |
-            /var/lib/apt/lists
-            !/var/lib/apt/lists/partial
-            !/var/lib/apt/lists/lock
-          key: apt-lists-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
-          restore-keys: |
-            apt-lists-${{ runner.os }}-
+      - name: Download and cache apt dependencies
+        run: |
+          mkdir -p ./cache/apt/archives
+          sudo apt-get update
+          apt-get download -o Dir::Cache::Archives="./cache/apt/archives" graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+
+      - name: Install apt dependencies from cache
+        if: steps.cache-apt.outputs.cache-hit != 'true'
+        run: |
+          sudo dpkg -i ./cache/apt/archives/*.deb || sudo apt-get install -f
 
       - name: Install blueprint apt dependencies
+        if: steps.cache-apt.outputs.cache-hit == 'true'
         run: |
           sudo apt-get update
-          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
-
-      - name: Cache blueprint dependencies
-        uses: actions/cache@v3
-        with:
-          path: ~/.cache/pip
-          key: blueprint-dependencies-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
-          restore-keys: |
-            blueprint-dependencies- # Cache Python dependencies for blueprint
+          sudo apt-get install -y ./cache/apt/archives/*.deb || sudo apt-get install -f
+
+      # - name: Cache blueprint dependencies
+      #   uses: actions/cache@v3
+      #   with:
+      #     path: ~/.cache/pip
+      #     key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
+      #     restore-keys: |
+      #       blueprint-dependencies- # Cache Python dependencies for blueprint
 
       - name: Install blueprint dependencies
         run: |

From cea305391c0b4f5e1d5cdd487f04531c33a068a0 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 10:06:26 +0200
Subject: [PATCH 10/42] Update push.yml

---
 .github/workflows/push.yml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index e6e3894..7886ead 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -34,7 +34,7 @@ jobs:
           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»
+        run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4
 
       - name: Get cache
         run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
@@ -81,6 +81,9 @@ jobs:
           sudo apt-get update
           apt-get download -o Dir::Cache::Archives="./cache/apt/archives" graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
 
+      - name: List cached files
+        run: ls -lh ./cache/apt/archives
+
       - name: Install apt dependencies from cache
         if: steps.cache-apt.outputs.cache-hit != 'true'
         run: |
@@ -92,13 +95,13 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y ./cache/apt/archives/*.deb || sudo apt-get install -f
 
-      # - name: Cache blueprint dependencies
-      #   uses: actions/cache@v3
-      #   with:
-      #     path: ~/.cache/pip
-      #     key: blueprint-dependencies-${{ hashFiles('blueprint/requirements.txt') }}
-      #     restore-keys: |
-      #       blueprint-dependencies- # Cache Python dependencies for blueprint
+      - name: Cache blueprint dependencies
+        uses: actions/cache@v3
+        with:
+          path: ~/.cache/pip
+          key: blueprint-dependencies-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
+          restore-keys: |
+            blueprint-dependencies- # Cache Python dependencies for blueprint
 
       - name: Install blueprint dependencies
         run: |

From 967c9e436ac4bfd5f8146d88d9446ad145238f99 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 10:41:02 +0200
Subject: [PATCH 11/42] Update push.yml

---
 .github/workflows/push.yml | 34 ++++++++++++++--------------------
 1 file changed, 14 insertions(+), 20 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 7886ead..b21c471 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -75,33 +75,27 @@ jobs:
           restore-keys: |
             apt-packages-
 
-      - name: Download and cache apt dependencies
+      - name: Download apt dependencies
+        if: steps.cache-apt.outputs.cache-hit != 'true'
         run: |
           mkdir -p ./cache/apt/archives
           sudo apt-get update
           apt-get download -o Dir::Cache::Archives="./cache/apt/archives" graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
-
-      - name: List cached files
-        run: ls -lh ./cache/apt/archives
+          ls -lh ./cache/apt/archives
 
       - name: Install apt dependencies from cache
-        if: steps.cache-apt.outputs.cache-hit != 'true'
-        run: |
-          sudo dpkg -i ./cache/apt/archives/*.deb || sudo apt-get install -f
-
-      - name: Install blueprint apt dependencies
-        if: steps.cache-apt.outputs.cache-hit == 'true'
         run: |
-          sudo apt-get update
-          sudo apt-get install -y ./cache/apt/archives/*.deb || sudo apt-get install -f
-
-      - name: Cache blueprint dependencies
-        uses: actions/cache@v3
-        with:
-          path: ~/.cache/pip
-          key: blueprint-dependencies-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
-          restore-keys: |
-            blueprint-dependencies- # Cache Python dependencies for blueprint
+          if [ -d "./cache/apt/archives" ]; then
+            sudo dpkg -i ./cache/apt/archives/*.deb || sudo apt-get install -f
+          fi
+
+      # - name: Cache blueprint dependencies
+      #   uses: actions/cache@v3
+      #   with:
+      #     path: ~/.cache/pip
+      #     key: blueprint-dependencies-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
+      #     restore-keys: |
+      #       blueprint-dependencies-
 
       - name: Install blueprint dependencies
         run: |

From 0fc58f39459e271f4df633b14fc40f7a786608f1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 11:05:02 +0200
Subject: [PATCH 12/42] Update push.yml

---
 .github/workflows/push.yml | 32 +++-----------------------------
 1 file changed, 3 insertions(+), 29 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index b21c471..09b1b06 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -66,36 +66,10 @@ jobs:
           python-version: '3.9'
           cache: 'pip'
 
-      - name: Cache apt packages
-        id: cache-apt
-        uses: actions/cache@v3
-        with:
-          path: ./cache/apt
-          key: apt-packages-${{ hashFiles('blueprint/requirements.txt') }}
-          restore-keys: |
-            apt-packages-
-
-      - name: Download apt dependencies
-        if: steps.cache-apt.outputs.cache-hit != 'true'
-        run: |
-          mkdir -p ./cache/apt/archives
-          sudo apt-get update
-          apt-get download -o Dir::Cache::Archives="./cache/apt/archives" graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
-          ls -lh ./cache/apt/archives
-
-      - name: Install apt dependencies from cache
+      - name: Install blueprint apt dependencies
         run: |
-          if [ -d "./cache/apt/archives" ]; then
-            sudo dpkg -i ./cache/apt/archives/*.deb || sudo apt-get install -f
-          fi
-
-      # - name: Cache blueprint dependencies
-      #   uses: actions/cache@v3
-      #   with:
-      #     path: ~/.cache/pip
-      #     key: blueprint-dependencies-${{ runner.os }}-${{ hashFiles('blueprint/requirements.txt') }}
-      #     restore-keys: |
-      #       blueprint-dependencies-
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
 
       - name: Install blueprint dependencies
         run: |

From 9c78d446e1800465816ba254b53c214d7e6218b4 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 11:12:09 +0200
Subject: [PATCH 13/42] Add useful comments

---
 .github/workflows/push.yml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 09b1b06..4d6cda7 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -15,6 +15,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: |
@@ -24,6 +25,7 @@ jobs:
     runs-on: ubuntu-latest
     name: Build project
     steps:
+
       - name: Checkout project
         uses: actions/checkout@v2
         with:
@@ -31,7 +33,7 @@ jobs:
 
       - 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 # Install Lean 4
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
 
       - name: Update docgen4
         run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4
@@ -42,6 +44,7 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis
 
+      # Cache the documentation for Mathlib to save rebuild time
       - name: Cache mathlib docs
         uses: actions/cache@v3
         with:
@@ -55,10 +58,10 @@ jobs:
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
-            MathlibDoc- # Cache Mathlib documentation to save rebuild time
+            MathlibDoc-
 
       - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
+        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 
       - name: Install Python
         uses: actions/setup-python@v4
@@ -66,6 +69,7 @@ jobs:
           python-version: '3.9'
           cache: 'pip'
 
+      # Install required apt packages for blueprint
       - name: Install blueprint apt dependencies
         run: |
           sudo apt-get update -qq
@@ -73,7 +77,7 @@ jobs:
 
       - name: Install blueprint dependencies
         run: |
-          cd blueprint && pip install -r requirements.txt # Install Python dependencies for blueprint
+          cd blueprint && pip install -r requirements.txt
 
       - name: Build blueprint and copy to `docs/blueprint`
         run: inv all
@@ -86,7 +90,7 @@ jobs:
       - 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
+          cp -r .lake/build/doc docs/docs
 
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
@@ -97,7 +101,7 @@ jobs:
 
       - name: Bundle website
         working-directory: docs
-        run: JEKYLL_ENV=production bundle exec jekyll build # Build the Jekyll site for production
+        run: JEKYLL_ENV=production bundle exec jekyll build
 
       - name: Upload docs & blueprint artifact
         uses: actions/upload-pages-artifact@v1

From b21f806b27ce2506d9757434ccf45f267202570d Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 11:23:44 +0200
Subject: [PATCH 14/42] Use `cache-apt-pkgs-action`

---
 .github/workflows/push.yml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 4d6cda7..9de4545 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -25,7 +25,6 @@ jobs:
     runs-on: ubuntu-latest
     name: Build project
     steps:
-
       - name: Checkout project
         uses: actions/checkout@v2
         with:
@@ -69,11 +68,13 @@ jobs:
           python-version: '3.9'
           cache: 'pip'
 
-      # Install required apt packages for blueprint
-      - name: Install blueprint apt dependencies
-        run: |
-          sudo apt-get update -qq
-          sudo apt-get install -y --no-install-recommends graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
+      # Cache and install required apt packages for blueprint
+      # graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
+      - name: Cache and install blueprint apt dependencies
+        uses: awalsh128/cache-apt-pkgs-action@latest
+        with:
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+          version: 1.0
 
       - name: Install blueprint dependencies
         run: |

From 40a900fde58280856ae4b1523e85979000a2ff3c Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 11:26:42 +0200
Subject: [PATCH 15/42] Minimal dependencies

---
 .github/workflows/push.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 9de4545..76b9d01 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -69,11 +69,10 @@ jobs:
           cache: 'pip'
 
       # Cache and install required apt packages for blueprint
-      # graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
           version: 1.0
 
       - name: Install blueprint dependencies

From b942750062761d99fa50adc96bd9718f146152fe Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 11:32:52 +0200
Subject: [PATCH 16/42] Test cache + minimal imports

---
 .github/workflows/push.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 76b9d01..2b761e1 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -69,6 +69,7 @@ jobs:
           cache: 'pip'
 
       # Cache and install required apt packages for blueprint
+      #graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:

From 9a5aaccdde2241591068bf4c9ffee126661f9790 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 11:56:42 +0200
Subject: [PATCH 17/42] Update push.yml

---
 .github/workflows/push.yml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 2b761e1..9cd2a64 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -69,13 +69,22 @@ jobs:
           cache: 'pip'
 
       # Cache and install required apt packages for blueprint
-      #graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
           packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
           version: 1.0
 
+      - name: Update TeX Live packages
+        run: |
+          sudo tlmgr update --self
+          sudo tlmgr update --all
+
+      # Ensure xelatex format file is generated
+      - name: Generate xelatex format file
+        run: |
+          sudo fmtutil-sys --all
+
       - name: Install blueprint dependencies
         run: |
           cd blueprint && pip install -r requirements.txt

From 415d58e7e776cd33c3a5b0716ab643b6c8a1ed0a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 12:01:47 +0200
Subject: [PATCH 18/42] Update push.yml

---
 .github/workflows/push.yml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 9cd2a64..82e19a3 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -75,14 +75,11 @@ jobs:
           packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
           version: 1.0
 
-      - name: Update TeX Live packages
+      # Update TeX Live packages and ensure XeLatex format file is generated
+      - name: Update TeX Live and generate XeLatex format file
         run: |
           sudo tlmgr update --self
           sudo tlmgr update --all
-
-      # Ensure xelatex format file is generated
-      - name: Generate xelatex format file
-        run: |
           sudo fmtutil-sys --all
 
       - name: Install blueprint dependencies

From 864e5a3d0d526e3bf5c19df797f091f7e97c3b0f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 12:36:30 +0200
Subject: [PATCH 19/42] Update push.yml

---
 .github/workflows/push.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 82e19a3..f77af88 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -78,7 +78,6 @@ jobs:
       # Update TeX Live packages and ensure XeLatex format file is generated
       - name: Update TeX Live and generate XeLatex format file
         run: |
-          sudo tlmgr update --self
           sudo tlmgr update --all
           sudo fmtutil-sys --all
 
@@ -117,4 +116,4 @@ jobs:
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
\ No newline at end of file
+        uses: actions/deploy-pages@v1

From c3654ffb4a8198dd60c5208d57068edb59a8bc44 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 12:37:17 +0200
Subject: [PATCH 20/42] Update push.yml

---
 .github/workflows/push.yml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index f77af88..7c92f5b 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -77,9 +77,7 @@ jobs:
 
       # Update TeX Live packages and ensure XeLatex format file is generated
       - name: Update TeX Live and generate XeLatex format file
-        run: |
-          sudo tlmgr update --all
-          sudo fmtutil-sys --all
+        run: sudo fmtutil-sys --all
 
       - name: Install blueprint dependencies
         run: |

From 81ca0ec09528edcf54c3be8a054a77da509b3a79 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 12:42:33 +0200
Subject: [PATCH 21/42] run `tlmgr ` in admin mode

---
 .github/workflows/push.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 82e19a3..1220185 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -78,6 +78,7 @@ jobs:
       # Update TeX Live packages and ensure XeLatex format file is generated
       - name: Update TeX Live and generate XeLatex format file
         run: |
+          sudo tlmgr init-usertree
           sudo tlmgr update --self
           sudo tlmgr update --all
           sudo fmtutil-sys --all

From 1b8437ab2be474d37d8544ea5560c670590f05c6 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 12:52:25 +0200
Subject: [PATCH 22/42] Update push.yml

---
 .github/workflows/push.yml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 393dc12..47ebcfc 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -75,13 +75,13 @@ jobs:
           packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
           version: 1.0
 
-      # Update TeX Live packages and ensure XeLatex format file is generated
-      - name: Update TeX Live and generate XeLatex format file
-        run: |
-          sudo tlmgr init-usertree
-          sudo tlmgr update --self
-          sudo tlmgr update --all
-          sudo fmtutil-sys --all
+      # # Update TeX Live packages and ensure XeLatex format file is generated
+      # - name: Update TeX Live and generate XeLatex format file
+      #   run: |
+      #     sudo tlmgr init-usertree
+      #     sudo tlmgr update --self
+      #     sudo tlmgr update --all
+      #     sudo fmtutil-sys --all
 
       - name: Install blueprint dependencies
         run: |

From 6ca7d1446501f48f08f88e4e31a71205ca85ab1c Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 13:02:05 +0200
Subject: [PATCH 23/42] Use `texlive-full`

---
 .github/workflows/push.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 47ebcfc..7cd0647 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -69,10 +69,12 @@ jobs:
           cache: 'pip'
 
       # Cache and install required apt packages for blueprint
+      #graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+      #graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
           version: 1.0
 
       # # Update TeX Live packages and ensure XeLatex format file is generated

From 3ba439c6b615223c5af74a3d073398f7fd2addbf Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 13:02:58 +0200
Subject: [PATCH 24/42] Update push.yml

---
 .github/workflows/push.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 7cd0647..3405241 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -78,6 +78,7 @@ jobs:
           version: 1.0
 
       # # Update TeX Live packages and ensure XeLatex format file is generated
+
       # - name: Update TeX Live and generate XeLatex format file
       #   run: |
       #     sudo tlmgr init-usertree

From c6033204c708028aa7b68e9ec488324029af0c3f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 13:12:33 +0200
Subject: [PATCH 25/42] Update push.yml

---
 .github/workflows/push.yml | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 3405241..251db30 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -69,23 +69,13 @@ jobs:
           cache: 'pip'
 
       # Cache and install required apt packages for blueprint
-      #graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
-      #graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
+      # graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
           version: 1.0
 
-      # # Update TeX Live packages and ensure XeLatex format file is generated
-
-      # - name: Update TeX Live and generate XeLatex format file
-      #   run: |
-      #     sudo tlmgr init-usertree
-      #     sudo tlmgr update --self
-      #     sudo tlmgr update --all
-      #     sudo fmtutil-sys --all
-
       - name: Install blueprint dependencies
         run: |
           cd blueprint && pip install -r requirements.txt
@@ -121,4 +111,4 @@ jobs:
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v1
\ No newline at end of file

From b0716d3172ee99552bc2fade80e0de285b94f848 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 13:40:40 +0200
Subject: [PATCH 26/42] Cache and install blueprint apt dependencies

---
 .github/workflows/push.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 251db30..d0b6e9c 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -69,11 +69,10 @@ jobs:
           cache: 'pip'
 
       # Cache and install required apt packages for blueprint
-      # graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
           version: 1.0
 
       - name: Install blueprint dependencies

From fe7556cb63b9783735641f79e449c7f72fa897be Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 14:27:51 +0200
Subject: [PATCH 27/42] Remove unnecessary comments

---
 .github/workflows/push.yml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index d0b6e9c..da8ba9e 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -15,7 +15,6 @@ 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: |
@@ -68,7 +67,6 @@ jobs:
           python-version: '3.9'
           cache: 'pip'
 
-      # Cache and install required apt packages for blueprint
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:

From ed6cb5a5ba9373b0bedb9bc8b7df27604327cc7f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 14:57:57 +0200
Subject: [PATCH 28/42] Reduced apt dependencies

---
 .github/workflows/push.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index da8ba9e..15355cf 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -70,7 +70,7 @@ jobs:
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
           version: 1.0
 
       - name: Install blueprint dependencies

From 14718a050934cdbe0da48d1c9ddc658888cf2344 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 15:10:40 +0200
Subject: [PATCH 29/42] Add effective dependencies

---
 .github/workflows/push.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 15355cf..17355ce 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -70,7 +70,7 @@ jobs:
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex latexmk biblatex
           version: 1.0
 
       - name: Install blueprint dependencies

From 839e815820286b123b610c637df9c9aa0c063b1e Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 15:26:58 +0200
Subject: [PATCH 30/42] Generate XeLaTeX format

---
 .github/workflows/push.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 17355ce..b748d60 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -77,6 +77,10 @@ jobs:
         run: |
           cd blueprint && pip install -r requirements.txt
 
+      - name: Generate XeLaTeX format
+        run: |
+          sudo fmtutil-sys --all
+
       - name: Build blueprint and copy to `docs/blueprint`
         run: inv all
 

From 444da3284f45e61c473e7062351b3313403b7dbd Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 15:37:19 +0200
Subject: [PATCH 31/42] Update push.yml

---
 .github/workflows/push.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index b748d60..bf08666 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -70,7 +70,7 @@ jobs:
       - name: Cache and install blueprint apt dependencies
         uses: awalsh128/cache-apt-pkgs-action@latest
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex latexmk biblatex
+          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex texlive-bibtex-extra latexmk biblatex
           version: 1.0
 
       - name: Install blueprint dependencies

From 7d6616010d68fd195a03e721c3437ca254b06540 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 16:17:17 +0200
Subject: [PATCH 32/42] Update push.yml

---
 .github/workflows/push.yml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index bf08666..f9c6990 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -77,12 +77,10 @@ jobs:
         run: |
           cd blueprint && pip install -r requirements.txt
 
-      - name: Generate XeLaTeX format
-        run: |
-          sudo fmtutil-sys --all
-
       - name: Build blueprint and copy to `docs/blueprint`
-        run: inv all
+        run: |
+          sudo fmtutil-sys --all # Generate XeLaTeX format
+          inv all
 
       - name: Remove lake files from documentation
         run: |

From fd63c990f9318efbd14f4c2a89451aaa57c53e4a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 6 Jul 2024 17:58:46 +0200
Subject: [PATCH 33/42] Update push.yml

---
 .github/workflows/push.yml | 56 ++++++++++++++++++++++----------------
 1 file changed, 33 insertions(+), 23 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index f9c6990..ac57954 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -15,6 +15,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: |
@@ -30,8 +31,7 @@ jobs:
           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 none
 
       - name: Update docgen4
         run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4
@@ -42,8 +42,7 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis
 
-      # Cache the documentation for Mathlib to save rebuild time
-      - name: Cache mathlib docs
+      - name: Cache mathlib documentation
         uses: actions/cache@v3
         with:
           path: |
@@ -58,36 +57,47 @@ jobs:
           restore-keys: |
             MathlibDoc-
 
-      - name: Build documentation
+      - name: Build project documentation
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 
-      - name: Install Python
-        uses: actions/setup-python@v4
-        with:
-          python-version: '3.9'
-          cache: 'pip'
-
-      - name: Cache and install blueprint apt dependencies
-        uses: awalsh128/cache-apt-pkgs-action@latest
+      - name: Cache blueprint environment
+        uses: actions/cache@v3
         with:
-          packages: graphviz libgraphviz-dev pdf2svg dvisvgm texlive-latex-base texlive-latex-extra texlive-fonts-recommended texlive-fonts-extra texlive-xetex texlive-bibtex-extra latexmk biblatex
-          version: 1.0
-
-      - name: Install blueprint dependencies
-        run: |
-          cd blueprint && pip install -r requirements.txt
+          path: |
+            ~/texlive-env
+          key: texlive-env-${{ hashFiles('blueprint/*') }}
+          restore-keys: |
+            texlive-env-
 
       - name: Build blueprint and copy to `docs/blueprint`
-        run: |
-          sudo fmtutil-sys --all # Generate XeLaTeX format
-          inv all
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv ~/texlive-env || true
+            source ~/texlive-env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install leanblueprint
+            leanblueprint pdf
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
+
+      # - name: Check declarations
+      #   run: |
+      #       ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
       - name: Remove lake files from documentation
         run: |
           find .lake/build/doc -name "*.trace" -delete
           find .lake/build/doc -name "*.hash" -delete
 
-      - name: Copy documentation to `docs/docs`
+      - name: Move documentation to `docs/docs`
         run: |
           sudo chown -R runner docs
           cp -r .lake/build/doc docs/docs

From 992d58f2e975ee74c02e2797834423cf9c27b0d2 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 7 Jul 2024 18:46:29 +0200
Subject: [PATCH 34/42] Bump doc-gen4

---
 .github/workflows/push.yml | 39 +++++++++++++++++---------------------
 lake-manifest.json         |  8 ++++----
 2 files changed, 21 insertions(+), 26 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index ac57954..1ea85e9 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -33,8 +33,8 @@ jobs:
       - name: Install elan
         run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
 
-      - name: Update docgen4
-        run: ~/.elan/bin/lake -R -Kenv=dev update doc-gen4
+      # - name: Update doc-gen4
+      #   run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
 
       - name: Get cache
         run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
@@ -54,32 +54,23 @@ jobs:
             .lake/build/doc/declarations
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            MathlibDoc-
+          #restore-keys: MathlibDoc-
 
       - name: Build project documentation
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 
-      - name: Cache blueprint environment
-        uses: actions/cache@v3
-        with:
-          path: |
-            ~/texlive-env
-          key: texlive-env-${{ hashFiles('blueprint/*') }}
-          restore-keys: |
-            texlive-env-
-
       - 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: |
+            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
             git config --global --add safe.directory `pwd`
-            python3 -m venv ~/texlive-env || true
-            source ~/texlive-env/bin/activate
+            python3 -m venv env
+            source env/bin/activate
             pip install --upgrade pip requests wheel
             pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
             pip install leanblueprint
@@ -88,16 +79,12 @@ jobs:
             leanblueprint web
             cp -r blueprint/web docs/blueprint
 
-      # - name: Check declarations
-      #   run: |
-      #       ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
-
       - name: Remove lake files from documentation
         run: |
           find .lake/build/doc -name "*.trace" -delete
           find .lake/build/doc -name "*.hash" -delete
 
-      - 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
@@ -113,11 +100,19 @@ jobs:
         working-directory: docs
         run: JEKYLL_ENV=production bundle exec jekyll build
 
-      - name: Upload docs & blueprint artifact
+      # - name: Upload docs & blueprint artifact to `docs/`
+      #   uses: actions/upload-pages-artifact@v1
+      #   with:
+      #     path: docs/
+
+      - name: Upload docs & blueprint artifact to `docs/_site`
         uses: actions/upload-pages-artifact@v1
         with:
           path: docs/_site
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
\ No newline at end of file
+        uses: actions/deploy-pages@v1
+
+      - name: Make sure the cache works
+        run: mv docs/docs .lake/build/doc
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index 2580094..ff60eda 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446",
+   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b387c548d1dc9cea5c5fcb71e5b3370cca1a04cc",
+   "rev": "363b8176ac29271af4b000b649f836c846f528fc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5cf3352cd6090e58c5ee878c786af8b87e8bdd65",
+   "rev": "7aa0886dc3f8dd486e00c19589d28c5bc0d7d860",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

From 0497e938b03b746bb909da41244f0ef6cdc5dd49 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 7 Jul 2024 23:15:41 +0200
Subject: [PATCH 35/42] Bump

---
 .github/workflows/push.yml | 8 ++++----
 lake-manifest.json         | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 1ea85e9..bbb88a8 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -79,10 +79,10 @@ jobs:
             leanblueprint web
             cp -r blueprint/web docs/blueprint
 
-      - name: Remove lake files from documentation
-        run: |
-          find .lake/build/doc -name "*.trace" -delete
-          find .lake/build/doc -name "*.hash" -delete
+      # - name: Remove lake files from documentation
+      #   run: |
+      #     find .lake/build/doc -name "*.trace" -delete
+      #     find .lake/build/doc -name "*.hash" -delete
 
       - name: Copy documentation to `docs/docs`
         run: |
diff --git a/lake-manifest.json b/lake-manifest.json
index ff60eda..f4925f8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
+   "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "363b8176ac29271af4b000b649f836c846f528fc",
+   "rev": "5943c0906d60d948ae848bd38430dc79ab013aa6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -102,4 +102,4 @@
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "bonnAnalysis",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake"}
\ No newline at end of file

From 1d27ace968c892e47d220eca003819f4e2f570ce Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 7 Jul 2024 23:57:30 +0200
Subject: [PATCH 36/42] Bump

---
 lake-manifest.json | 72 +++++++++++++++++++++++-----------------------
 1 file changed, 36 insertions(+), 36 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index f4925f8..97f4ee6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446",
+   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,41 +65,41 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5943c0906d60d948ae848bd38430dc79ab013aa6",
+   "rev": "38e09f6c5663173303181f2e3ac0c922f9f2eb2f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "c74a052aebee847780e165611099854de050adf7",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "7aa0886dc3f8dd486e00c19589d28c5bc0d7d860",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
- "name": "bonnAnalysis",
- "lakeDir": ".lake"}
\ No newline at end of file
+   {"url": "https://github.com/acmepjz/md4lean",
+    "type": "git",
+    "subDir": null,
+    "scope": "",
+    "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+    "name": "MD4Lean",
+    "manifestFile": "lake-manifest.json",
+    "inputRev": "main",
+    "inherited": true,
+    "configFile": "lakefile.lean"},
+   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+    "type": "git",
+    "subDir": null,
+    "scope": "",
+    "rev": "c74a052aebee847780e165611099854de050adf7",
+    "name": "UnicodeBasic",
+    "manifestFile": "lake-manifest.json",
+    "inputRev": "main",
+    "inherited": true,
+    "configFile": "lakefile.lean"},
+   {"url": "https://github.com/leanprover/doc-gen4",
+    "type": "git",
+    "subDir": null,
+    "scope": "",
+    "rev": "d1be57c7fbd80ac20584ed0a86a2165c62cd993b",
+    "name": "«doc-gen4»",
+    "manifestFile": "lake-manifest.json",
+    "inputRev": "main",
+    "inherited": false,
+    "configFile": "lakefile.lean"}],
+  "name": "carleson",
+  "lakeDir": ".lake"}

From f1afc15972b6732dc4e9d329dc79705a3849da93 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 00:26:31 +0200
Subject: [PATCH 37/42] Remove lake files from documentation

---
 .github/workflows/push.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index bbb88a8..1ea85e9 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -79,10 +79,10 @@ jobs:
             leanblueprint web
             cp -r blueprint/web docs/blueprint
 
-      # - name: Remove lake files from documentation
-      #   run: |
-      #     find .lake/build/doc -name "*.trace" -delete
-      #     find .lake/build/doc -name "*.hash" -delete
+      - name: Remove lake files from documentation
+        run: |
+          find .lake/build/doc -name "*.trace" -delete
+          find .lake/build/doc -name "*.hash" -delete
 
       - name: Copy documentation to `docs/docs`
         run: |

From 6a1486d9f4162c43e26b5b8e84ca449670f71839 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 00:49:43 +0200
Subject: [PATCH 38/42] Update push.yml

---
 .github/workflows/push.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 1ea85e9..d41999a 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -2,7 +2,6 @@ on:
   push:
     branches:
       - master
-      - gh-actions
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:

From 2477ed724a25db971d0847714d1181f2d91a8590 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 12:23:27 +0200
Subject: [PATCH 39/42] Add `restore-keys`

---
 .github/workflows/push.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index d41999a..0605b24 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -53,7 +53,7 @@ jobs:
             .lake/build/doc/declarations
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
-          #restore-keys: MathlibDoc-
+          restore-keys: MathlibDoc-
 
       - name: Build project documentation
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs

From 289c227ceac521f0bee95e2f0fa784ab319d49c6 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 13:10:43 +0200
Subject: [PATCH 40/42] Fix manifest

---
 .github/workflows/push.yml | 1 +
 lake-manifest.json         | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 0605b24..d0584f1 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -2,6 +2,7 @@ on:
   push:
     branches:
       - master
+      - gh-actions
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
diff --git a/lake-manifest.json b/lake-manifest.json
index 97f4ee6..369eaca 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "38e09f6c5663173303181f2e3ac0c922f9f2eb2f",
+   "rev": "b387c548d1dc9cea5c5fcb71e5b3370cca1a04cc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -101,5 +101,5 @@
     "inputRev": "main",
     "inherited": false,
     "configFile": "lakefile.lean"}],
-  "name": "carleson",
+  "name": "bonnAnalysis",
   "lakeDir": ".lake"}

From c3cb053d175c87941ccee1d3e003964e3177307a Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 13:52:54 +0200
Subject: [PATCH 41/42] Revert manifest + update doc-gen

---
 .github/workflows/push.yml |  1 -
 lake-manifest.json         | 40 +++++---------------------------------
 2 files changed, 5 insertions(+), 36 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index d0584f1..0605b24 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -2,7 +2,6 @@ on:
   push:
     branches:
       - master
-      - gh-actions
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
diff --git a/lake-manifest.json b/lake-manifest.json
index 369eaca..5690e57 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
+   "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -70,36 +70,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-   {"url": "https://github.com/acmepjz/md4lean",
-    "type": "git",
-    "subDir": null,
-    "scope": "",
-    "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
-    "name": "MD4Lean",
-    "manifestFile": "lake-manifest.json",
-    "inputRev": "main",
-    "inherited": true,
-    "configFile": "lakefile.lean"},
-   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-    "type": "git",
-    "subDir": null,
-    "scope": "",
-    "rev": "c74a052aebee847780e165611099854de050adf7",
-    "name": "UnicodeBasic",
-    "manifestFile": "lake-manifest.json",
-    "inputRev": "main",
-    "inherited": true,
-    "configFile": "lakefile.lean"},
-   {"url": "https://github.com/leanprover/doc-gen4",
-    "type": "git",
-    "subDir": null,
-    "scope": "",
-    "rev": "d1be57c7fbd80ac20584ed0a86a2165c62cd993b",
-    "name": "«doc-gen4»",
-    "manifestFile": "lake-manifest.json",
-    "inputRev": "main",
-    "inherited": false,
-    "configFile": "lakefile.lean"}],
-  "name": "bonnAnalysis",
-  "lakeDir": ".lake"}
+   "configFile": "lakefile.lean"}],
+ "name": "bonnAnalysis",
+ "lakeDir": ".lake"}

From 931786021756546560c27d395f7decf09aefc6e2 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 14:05:04 +0200
Subject: [PATCH 42/42] Update doc-gen

---
 lake-manifest.json | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/lake-manifest.json b/lake-manifest.json
index 5690e57..f393146 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -70,6 +70,36 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c74a052aebee847780e165611099854de050adf7",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "194403be8599ce1d95afa15113960045f8483c7c",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "bonnAnalysis",
  "lakeDir": ".lake"}