diff --git a/lake-manifest.json b/lake-manifest.json
index 887384d..60dd202 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,15 +4,9 @@
  [{"git":
    {"url": "https://github.com/xubaiw/CMark.lean",
     "subDir?": null,
-    "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8",
+    "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
     "name": "CMark",
     "inputRev?": "main"}},
-  {"git":
-   {"url": "https://github.com/leanprover/lake",
-    "subDir?": null,
-    "rev": "0d4da61cbfe65f19ac7070c2c9f62f36db529c4c",
-    "name": "lake",
-    "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli",
     "subDir?": null,
@@ -28,6 +22,6 @@
   {"git":
    {"url": "https://github.com/fgdorais/lean4-unicode-basic",
     "subDir?": null,
-    "rev": "ce508dcd1fd49ba15675861aafd864572a0b8252",
+    "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
     "name": "UnicodeBasic",
     "inputRev?": "main"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index c0146b8..bc1253e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -20,9 +20,6 @@ require UnicodeBasic from git
 require Cli from git
   "https://github.com/mhuisi/lean4-cli" @ "nightly"
 
-require lake from git
-  "https://github.com/leanprover/lake" @ "master"
-
 require leanInk from git
   "https://github.com/hargonix/LeanInk" @ "doc-gen"
 
@@ -70,8 +67,7 @@ library_facet docs (lib) : FilePath := do
   let exeJob ← docGen4.exe.fetch
 
   -- XXX: Workaround remove later
-  let coreJob ← if h : docGen4Pkg.name = _package.name then
-    have : PackageName docGen4Pkg _package.name := ⟨h⟩
+  let coreJob ← if docGen4Pkg.name = _package.name then
     let job := fetch <| docGen4Pkg.target `coreDocs
     job
   else
diff --git a/lean-toolchain b/lean-toolchain
index 02773ff..efc56ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-31
+leanprover/lean4:nightly-2023-07-29