[CI]: fix docs generation (#359)

* Update build_docs.sh

* Update blueprint.yml

* Update build_docs.sh

* Update build_docs.sh

* Update build_docs.sh

* Update build_docs.sh

* Update build_docs.sh

* test

* test

* test

* test

* test website generation

* fix github metadata warning

* Update build_docs.sh

* add set -euo pipefail

.github/workflows/blueprint.yml

@@ -9,6 +9,7 @@ on:
       - '**/blueprint.yml'
       - 'blueprint/**'
       - 'docs/**'
+      - 'scripts/**'
       - 'lean-toolchain'
       - 'lakefile.toml'
       - 'lake-manifest.json'
@@ -20,6 +21,7 @@ on:
       - '**/blueprint.yml'
       - 'blueprint/**'
       - 'docs/**'
+      - 'scripts/**'
       - 'lean-toolchain'
       - 'lakefile.toml'
       - 'lake-manifest.json'
@@ -74,7 +76,7 @@ jobs:
       - name: Cache Mathlib docs
         uses: actions/cache@v4
         with:
-          path: docs/docs
+          path: docbuild/.lake/build/doc
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             MathlibDoc-
@@ -112,8 +114,7 @@ jobs:
             cp -r blueprint/web docs/blueprint
 
       - name: Check declarations mentioned in the blueprint exist in Lean code
-        run: |
-            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+        run: ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
       - name: Build project API documentation
         run: scripts/build_docs.sh
@@ -129,6 +130,8 @@ jobs:
       - name: Build website using Jekyll
         if: github.event_name == 'push' && env.DOCS_EXISTS == 'true'
         working-directory: docs
+        env:
+            JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: JEKYLL_ENV=production bundle exec jekyll build  # Note this will also copy the blueprint and API doc into docs/_site
 
       - name: "Upload website (API documentation, blueprint and any home page)"

scripts/build_docs.sh

@@ -1,3 +1,9 @@
+#!/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 FLT
 # The output will be located in docs/docs
 
@@ -29,22 +35,16 @@ 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
 
-# Fetch the docs cache if it exists
-mkdir -p docs/docs
-mv docs/docs docbuild/.lake/build/doc
-
 # Initialise docbuild as a Lean project
 cd docbuild
-MATHLIB_NO_CACHE_ON_UPDATE=1 # Disable an error message due to a non-blocking bug. See Zulip
-~/.elan/bin/lake update FLT
-~/.elan/bin/lake exe cache get
+
+# Disable an error message due to a non-blocking bug. See Zulip
+MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update FLT
 
 # Build the docs
 ~/.elan/bin/lake build FLT:docs
 
-# Move them out of docbuild
+# Copy documentation to `docs/docs`
 cd ../
-mv docbuild/.lake/build/doc docs/docs
-
-# Clean up after ourselves
-rm -rf docbuild
+sudo chown -R runner docs
+cp -r docbuild/.lake/build/doc docs/docs