From 8cb4ee0f517bd1cd41f50c7e44da890cfab67d04 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 8 Jul 2024 14:27:22 +0200
Subject: [PATCH] Speed up CI (#34)

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

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 6727a41..0605b24 100644
--- a/.github/workflows/push.yml
+++ b/.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,11 +30,10 @@ 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 # Install Lean 4
+        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
@@ -41,7 +41,7 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis
 
-      - name: Cache mathlib docs
+      - name: Cache mathlib documentation
         uses: actions/cache@v3
         with:
           path: |
@@ -53,29 +53,30 @@ jobs:
             .lake/build/doc/declarations
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            MathlibDoc- # Cache Mathlib documentation to save rebuild time
-
-      - 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'
-
-      - name: Install blueprint apt dependencies
-        run: |
-          sudo apt-get update
-          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
+          restore-keys: MathlibDoc-
 
-      - name: Install blueprint dependencies
-        run: |
-          cd blueprint && pip install -r requirements.txt # Install Python dependencies for blueprint
+      - name: Build project documentation
+        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 
       - name: Build blueprint and copy to `docs/blueprint`
-        run: inv all
+        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 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
+            leanblueprint pdf
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
 
       - name: Remove lake files from documentation
         run: |
@@ -85,7 +86,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
@@ -96,13 +97,21 @@ 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
+      # - 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..f393146 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5cf3352cd6090e58c5ee878c786af8b87e8bdd65",
+   "rev": "194403be8599ce1d95afa15113960045f8483c7c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",