diff --git a/CLAUDE.md b/CLAUDE.md index 3cb930f1..58dbc474 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -177,4 +177,8 @@ See CONTRIBUTING.md. Use `(): ` 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". diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index 7d31fe22..372ae65e 100644 --- a/docbuild/lake-manifest.json +++ b/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", diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index 4955867f..f497bba4 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -18,4 +18,4 @@ path = ".." [[require]] scope = "leanprover" name = "doc-gen4" -rev = "v4.30.0" +rev = "v4.34.0-rc2" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain index af9e5d33..b814d987 100644 --- a/docbuild/lean-toolchain +++ b/docbuild/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0 +leanprover/lean4:v4.34.0-rc2