diff --git a/.gitignore b/.gitignore
index 2ee099a..bfb30ec 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1 @@
-/build
-/lake-packages
+/.lake
diff --git a/lake-manifest.json b/lake-manifest.json
index 8e96c47..97b04d0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,15 +1,23 @@
-{"version": 4,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
-    "name": "Qq",
-    "inputRev?": "master"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8",
-    "name": "std",
-    "inputRev?": "main"}}]}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "ae9ae7f279421e45a9b87d67f2d28aaef299de5c",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/gebner/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "iris",
+ "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index e183d2c..cfcdd32 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-30
+leanprover/lean4:v4.6.0-rc1