CI: generate doc-building repository in CI (#334)

* CI: regenerate doc-building repository in CI
* Don't have `docbuild` lying around always. Currently, the toolchain it gets updated to is independent of the toolchain FLT is on, causing issue every first few days of the month. Now, the toolchain with which the docs are built will always be the one from FLT. No one anymore can accidentally introduce a toolchain mismatch error in the repo by modifying/forgetting to modify the pinned toolchain in `docbuild/lakefile.toml`.
* Add `scripts/build_docs.sh` to automate building the docs. This script creates a temporary `docbuild` repo, generates the docs, then deletes the temporary repo again.
* Remove `scripts/bump.sh`. Now that `docbuild` doesn't exist outside of CI/building the docs locally with `build_docs.sh`, instructions to update the repo are simply "Run `lake update`".

* Remove working directory

* typo

Co-authored-by: Pietro Monticone <[email protected]>

* MATHLIB_NO_CACHE_ON_UPDATE

---------

Co-authored-by: Pietro Monticone <[email protected]>

.github/workflows/blueprint.yml

@@ -79,12 +79,6 @@ jobs:
           restore-keys: |
             MathlibDoc-
 
-      - name: Build project API documentation
-        working-directory: docbuild
-        run: |
-          MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update FLT || true
-          ~/.elan/bin/lake build FLT:docs
-
       - name: Check for `docs` folder # this is meant to detect a Jekyll-based website
         id: check_docs
         run: |
@@ -121,8 +115,8 @@ jobs:
         run: |
             ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
 
-      - name: Copy API documentation to `docs/docs`
-        run: cp -r docbuild/.lake/build/doc docs/docs
+      - name: Build project API documentation
+        run: scripts/build_docs.sh
 
       - name: Bundle dependencies
         if: github.event_name == 'push'

.gitignore

@@ -3,6 +3,8 @@
 /lake-packages/*
 .lake/*
 .DS_Store
+# Documentation
+docs/build
 # Lean blueprint
 blueprint/print/print.log
 blueprint/web/

scripts/build_docs.sh

@@ -0,0 +1,46 @@
+# Build HTML documentation for FLT
+# 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 = "FLT"
+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
+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
+
+# Build the docs
+~/.elan/bin/lake build FLT:docs
+
+# Move them out of docbuild
+cd ../
+mv docbuild/.lake/build/doc docs/docs
+
+# Clean up after ourselves
+rm -rf docbuild