From 09dbebed9ca85368152bb5146ef6f1271b1be425 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 4 Jan 2023 23:40:48 +0100
Subject: [PATCH] chore: QoL updates for deploy_docs.sh

---
 .github/workflows/build.yml | 4 ++++
 deploy_docs.sh              | 9 ++++++---
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 8c1a7c7..60baefa 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -23,6 +23,10 @@ jobs:
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
+      - name: Compile doc-gen4
+        run: |
+          lake build
+
       - name: Checkout and compile mathlib4
         run: |
           cd ../
diff --git a/deploy_docs.sh b/deploy_docs.sh
index 070980e..61f1a99 100755
--- a/deploy_docs.sh
+++ b/deploy_docs.sh
@@ -6,6 +6,7 @@
 set -e
 set -x
 
+cp -r $2/lake-packages/* $1/lake-packages
 cd $1
 mathlib_short_git_hash="$(git log -1 --pretty=format:%h)"
 
@@ -23,10 +24,12 @@ fi
 
 # generate the docs
 cd $1
-sed -i "s|\"https://github.com/leanprover/doc-gen4\" @ \"main\"|\"$DOC_GEN_URL\" @ \"$DOC_GEN_REF\"|" lakefile.lean
-rm -rf lean_packages/manifest.json
+sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\" with NameMap.empty|" lakefile.lean
+# This can destroy caching properties if std4 or aesop master are out of sync with mathlib4 but
+# we need it since lake does not provide the ability to update singular deps
+# right now. Once the feature is implemented we can stop doing that.
 lake -Kdoc=on update
-lake -Kdoc=on build Mathlib:docs Std:docs --verbose
+lake -Kdoc=on build Mathlib:docs Std:docs
 
 if [ "$3" = "true" ]; then
   cd ..