From 2f12c9525899e6118f5d5a56f23e5033b753539b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 3 Oct 2024 15:05:38 +0000
Subject: [PATCH] Update workflow

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

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 727648df84..bd09a30e50 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -45,13 +45,13 @@ jobs:
         run: python scripts/count_sorry.py
 
       - 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.5.0
 
       - name: Get cache
-        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+        run: ~/.elan/bin/lake exe cache get || true
 
       - name: Build project
-        run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP
+        run: ~/.elan/bin/lake build LeanAPAP
 
       - name: Cache mathlib docs
         uses: actions/cache@v3
@@ -68,26 +68,28 @@ jobs:
             MathlibDoc-
 
       - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP:docs
+        run: ~/.elan/bin/lake -R -Kenv=dev build LeanAPAP: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: |
-            export PIP_BREAK_SYSTEM_PACKAGES=1
             apk update
-            apk add --update make py3-pip git
             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 pip install --upgrade pip requests wheel
-            python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
-            pip install -r blueprint/requirements.txt
-            python3 -m pip install invoke
-            inv all
-
-      - name: Copy documentation to `docs/docs`
+            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: Move documentation to `docs/docs`
         run: |
           mv .lake/build/doc docs/docs
 
@@ -95,12 +97,12 @@ jobs:
         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"  # Specify Ruby version
+          bundler-cache: true  # Enable caching for bundler
 
-      - name: Bundle website
+      - name: Build website using Jekyll
         working-directory: docs
-        run: JEKYLL_ENV=production bundle exec jekyll build
+        run: JEKYLL_ENV=production bundle exec jekyll build  # Note this will also copy the blueprint and API doc into docs/_site
 
       - name: Upload docs & blueprint artifact
         uses: actions/upload-pages-artifact@v1
@@ -111,6 +113,10 @@ jobs:
         id: deployment
         uses: actions/deploy-pages@v1
 
+      - name: Check declarations
+        run: |
+            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
       - name: Make sure the cache works
         run: |
           mv docs/docs .lake/build/doc