chore: upgrade doc-gen workflow (#253)

For context read [this Zulip
topic](https://leanprover.zulipchat.com/#narrow/channel/303200-sphere-eversion/topic/Mathlib.20bumps/near/503257037).

Author: pitmonticone

.github/workflows/push.yml

@@ -59,17 +59,10 @@ jobs:
       - name: Cache API docs
         uses: actions/cache@v4
         with:
-          path: |
-            docbuild/.lake/build/doc
-          key: LakeBuildDoc-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          path: docbuild/.lake/build/doc
+          key: LakeBuildDoc-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
           restore-keys: LakeBuildDoc-
 
-      - name: Build project documentation
-        working-directory: docbuild
-        run: |
-          MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update carleson || true
-          ~/.elan/bin/lake build Carleson:docs
-
       - name: Build blueprint and copy to `docs/blueprint`
         uses: xu-cheng/texlive-action@v2
         with:
@@ -93,15 +86,8 @@ jobs:
       - name: Check declarations
         run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
-      - name: Copy documentation to `docs/docs`
-        run: |
-          sudo chown -R runner docs
-          cp -r docbuild/.lake/build/doc docs/docs
-
-      # - name: Remove lake files from documentation in `docs/docs`
-      #   run: |
-      #     find docs/docs -name "*.trace" -delete
-      #     find docs/docs -name "*.hash" -delete
+      - name: Build project API documentation
+        run: scripts/build_docs.sh
 
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1

.github/workflows/push_pr.yml

@@ -29,10 +29,12 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake build Carleson
 
-      - name: Test carleson update in docbuild
-        working-directory: docbuild
-        run: |
-          MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update carleson || true
+      - name: Cache API docs
+        uses: actions/cache@v4
+        with:
+          path: docbuild/.lake/build/doc
+          key: LakeBuildDoc-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: LakeBuildDoc-
 
       - name: Build blueprint and copy to `docs/blueprint`
         uses: xu-cheng/texlive-action@v2
@@ -54,3 +56,6 @@ jobs:
 
       - name: Check declarations
         run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
+      - name: Build project API documentation
+        run: scripts/build_docs.sh

docbuild/.gitignore

@@ -0,0 +1,50 @@
+#!/usr/bin/env bash
+
+# Exit immediately if a command exits with a non-zero status,
+# treat unset variables as an error, and ensure errors in pipelines are not masked.
+set -euo pipefail
+
+# Build HTML documentation for Carleson
+# The output will be located in docs/docs
+
+# Template lakefile.toml
+template() {
+  cat <<EOF
+name = "docbuild"
+reservoir = false
+version = "0.1.0"
+packagesDir = "../.lake/packages"
+
+[[require]]
+name = "carleson"
+path = "../"
+
+[[require]]
+scope = "leanprover"
+name = "doc-gen4"
+rev = "TOOLCHAIN"
+EOF
+}
+
+# Create a temporary docbuild folder
+mkdir -p docbuild
+
+# Equip docbuild with the template lakefile.toml
+template > docbuild/lakefile.toml
+
+# Substitute the toolchain from lean-toolchain into docbuild/lakefile.toml
+sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
+
+# Initialise docbuild as a Lean project
+cd docbuild
+
+# Disable an error message due to a non-blocking bug. See Zulip
+MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update carleson
+
+# Build the docs
+~/.elan/bin/lake build Carleson:docs
+
+# Copy documentation to `docs/docs`
+cd ../
+sudo chown -R runner docs
+cp -r docbuild/.lake/build/doc docs/docs