From fec289d5c51c8b97cdfa772386ddc5d2dcdc43f8 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 21 Nov 2024 20:57:54 +0100
Subject: [PATCH] fix "Build project documentation" job step

---
 .github/workflows/push.yml  |  2 +-
 docbuild/lake-manifest.json | 30 +++++++++++++++---------------
 docbuild/lean-toolchain     |  2 +-
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index f3cbfd7b..fc83010e 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -76,7 +76,7 @@ jobs:
       - name: Build project documentation
         working-directory: docbuild
         run: |
-          ~/.elan/bin/lake exe cache get || true
+          ~/.elan/bin/lake update carleson || true
           ~/.elan/bin/lake build Carleson:docs
 
       - name: Build blueprint and copy to `docs/blueprint`
diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
index a88817e7..81bc9720 100644
--- a/docbuild/lake-manifest.json
+++ b/docbuild/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "rev": "a822446d61ad7e7f5e843365c7041c326553050a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,17 +35,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.44",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841",
+   "rev": "840e02ce2768e06de7ced0a624444746590e9d99",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "stable",
+   "inputRev": null,
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -122,7 +122,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96",
+   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -132,7 +132,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
+   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -142,10 +142,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5",
+   "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "docbuild",
diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain
index 4f86f953..57a4710c 100644
--- a/docbuild/lean-toolchain
+++ b/docbuild/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0-rc2