CI changes coming from add-combi

* Replace `lakefile.toml` by `lakefile.lean`
* Acquire `scripts/build_docs.sh`
* Drop `scripts/bump.sh`

Author: YaelDillies

.github/workflows/push_master.yml

@@ -61,19 +61,15 @@ jobs:
           sudo apt install graphviz -y
           ~/.elan/bin/lake exe graph website/file_deps.pdf
 
-      - name: Cache dependencies docs
-        uses: actions/cache@v3
+      - name: Cache documentation
+        uses: actions/cache@v4
         with:
-          path: docbuild/.lake/build/doc
+          path: docs/docs
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            MathlibDoc-
+          restore-keys: MathlibDoc-
 
       - name: Build documentation
-        working-directory: docbuild
-        run: |
-          ~/.elan/bin/lake exe cache get || true
-          ~/.elan/bin/lake build LeanCamCombi:docs
+        run: scripts/build_docs.sh
 
       # - name: Build blueprint and copy to `website/blueprint`
       #   uses: xu-cheng/texlive-action@v2
@@ -91,8 +87,7 @@ jobs:
       #       inv all
 
       - name: Copy documentation to `website/docs`
-        run: |
-          mv docbuild/.lake/build/doc website/docs
+        run: mv docs/build website/docs
 
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1

docbuild/lake-manifest.json

@@ -0,0 +1,15 @@
+name = "LeanCamCombi"
+defaultTargets = ["LeanCamCombi"]
+
+[leanOptions]
+autoImplicit = false        # Prevent typos to be interpreted as new free variables
+relaxedAutoImplicit = false
+pp.unicode.fun = true       # Pretty-print lambdas as `fun a ↦ b`
+pp.proofs.withType = false  # Elide the types of proofs in terms
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+
+[[lean_lib]]
+name = "LeanCamCombi"

docbuild/lakefile.toml

@@ -0,0 +1,50 @@
+# Build HTML documentation for add-combi
+# The output will be located in docs/build
+
+# Template lakefile.toml
+template() {
+  cat <<EOF
+name = "docbuild"
+reservoir = false
+version = "0.1.0"
+packagesDir = "../.lake/packages"
+
+[[require]]
+name = "LeanCamCombi"
+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
+
+# 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 LeanCamCombi
+~/.elan/bin/lake exe cache get
+
+# Build the docs
+~/.elan/bin/lake build LeanCamCombi:docs
+
+# Move them out of docbuild
+cd ../
+mv docbuild/.lake/build/doc docs/build
+
+# Clean up after ourselves
+rm -rf docbuild