build(docs): align docbuild pins with root toolchain and add cslib

CLAUDE.md

@@ -177,4 +177,8 @@ See CONTRIBUTING.md. Use `<type>(<scope>): <summary>` format with imperative moo
   no olean cache; Lake compiles only the cslib modules we import.
 
 When updating any of the three, all must be updated in lockstep: pick the cslib commit first, then
-take its `lean-toolchain` and Mathlib `rev`.
+take its `lean-toolchain` and Mathlib `rev`. The `docbuild/` subproject pins the same toolchain
+separately: bump `docbuild/lean-toolchain` and the `doc-gen4` `rev` (tagged per Lean release) in
+`docbuild/lakefile.toml`, then regenerate its manifest with
+`cd docbuild && MATHLIB_NO_CACHE_ON_UPDATE=1 lake update`. Any new root dependency also needs this
+regeneration or the docs workflow fails with "not in manifest".

docbuild/lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "689fdeecf45e08cc048214680d40cfe2491be78b",
+   "rev": "97d4ecdfc8e09e7f511724c25e303d448de6a3db",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.34.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
@@ -22,7 +22,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a1d21d8b5f230205bb04c3bff479383f66802c0b",
+   "rev": "fdb62324e6f06eeb31ff4b81e46e030f40045250",
    "name": "leansqlite",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f8c99ff779ec217063545b3b191747c92e7fbfb3",
+   "rev": "bbb75c5c9b7f30d5e397f27bd099655aed7db410",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,37 +52,47 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539",
+   "rev": "4cd1575ab202c7b2b59d8c3eb4b792744e9988fc",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/cslib",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d9be64196bf145edd019f1ccfeaee0c11166ba6b",
+   "name": "cslib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "d9be64196bf145edd019f1ccfeaee0c11166ba6b",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+   "rev": "e06eff5f95374108acfaf19f1ff7473aa7771df2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "e06eff5f95374108acfaf19f1ff7473aa7771df2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,7 +102,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "ba67e212be1197b84c1f1f6299488a10a3002713",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -102,7 +112,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "rev": "d8823026ac7ef130c253089d95685f9877b95323",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -112,37 +122,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+   "rev": "7e23602c91bc04586b2b06de2708a041853e4681",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

docbuild/lakefile.toml

@@ -18,4 +18,4 @@ path = ".."
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.30.0"
+rev = "v4.34.0-rc2"

docbuild/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.30.0
+leanprover/lean4:v4.34.0-rc2