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] 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",