diff --git a/lake-manifest.json b/lake-manifest.json
index ce1062a4..2d539cc3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/xubaiw/CMark.lean",
    "type": "git",
    "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
    "name": "CMark",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "5b096942260d7805cc90bacf4ea4a0f8e9700ccb",
+   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/mhuisi/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+   "rev": "10d88b52fa8d717fa8e29af3abf0c3a2bf175497",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly",
@@ -40,7 +40,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "780bbec107cba79d18ec55ac2be3907a77f27f98",
+   "rev": "35f0efcffd023ec47fcf9a76a798b9c60a3720e3",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0783e9ceae1c8c11957fb5e0fe3e70fd2d43eea2",
+   "rev": "80cf5a1f2d8ed48753e8ff783bf0f7b6872bb007",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -67,7 +67,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -76,16 +76,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.35",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "188eb34fcf1125e89d651ad462d02598219718ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "ac1182835d2d1cb42c76a0f4b60c42183b5c8ed9",
+   "rev": "ff35083cb67970f88d9a6b2c14d06fdf299b6d30",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index e35881ce..d8a6d7ef 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc2
+leanprover/lean4:v4.8.0-rc1