From 51bb1bae470b408b4f87a049a9493532fc46fa81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= <anders@sorby.xyz>
Date: Mon, 25 Dec 2023 15:37:04 +0100
Subject: [PATCH] chore: Use lean v4.4.0

---
 .gitignore         |  1 +
 lake-manifest.json | 74 +++++++++++++++++++++++++---------------------
 lakefile.lean      |  6 ++--
 lean-toolchain     |  2 +-
 4 files changed, 45 insertions(+), 38 deletions(-)

diff --git a/.gitignore b/.gitignore
index 7c71214..bfc51a1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 /build
 /lake-packages
+/.lake
 
 # Ignore nix stuff, just in case?
 /result
diff --git a/lake-manifest.json b/lake-manifest.json
index 8143464..2b5b323 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,35 +1,41 @@
-{"version": 5,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/lurk-lab/YatimaStdLib.lean",
-    "subDir?": null,
-    "rev": "5b64c5150e371fb280728cbb5b7c225b9c96b348",
-    "opts": {},
-    "name": "YatimaStdLib",
-    "inputRev?": "5b64c5150e371fb280728cbb5b7c225b9c96b348",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/lurk-lab/straume",
-    "subDir?": null,
-    "rev": "053d9feccbface9a0b2c1a72447914376aac74ea",
-    "opts": {},
-    "name": "Straume",
-    "inputRev?": "053d9feccbface9a0b2c1a72447914376aac74ea",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/lurk-lab/LSpec",
-    "subDir?": null,
-    "rev": "3b6023654b917c8641ec5e626724a43380cff8f0",
-    "opts": {},
-    "name": "LSpec",
-    "inputRev?": "3b6023654b917c8641ec5e626724a43380cff8f0",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4/",
-    "subDir?": null,
-    "rev": "642cbc9960b49a65a779b8fce56b05ff83cf9e35",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "642cbc9960b49a65a779b8fce56b05ff83cf9e35",
-    "inherited": true}}]}
+ [{"url": "https://github.com/lurk-lab/LSpec",
+   "type": "git",
+   "subDir": null,
+   "rev": "3b6023654b917c8641ec5e626724a43380cff8f0",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3b6023654b917c8641ec5e626724a43380cff8f0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/std4/",
+   "type": "git",
+   "subDir": null,
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/lurk-lab/YatimaStdLib.lean",
+   "type": "git",
+   "subDir": null,
+   "rev": "3037f0c14128751b95510c2723f067ec7a494f08",
+   "name": "YatimaStdLib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3037f0c14128751b95510c2723f067ec7a494f08",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/lurk-lab/straume",
+   "type": "git",
+   "subDir": null,
+   "rev": "ad2aa666b7e4148df450ecf74aedb477f1535534",
+   "name": "Straume",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "ad2aa666b7e4148df450ecf74aedb477f1535534",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Megaparsec",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index cefb27c..915d028 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,13 +7,13 @@ package Megaparsec
 lean_lib Megaparsec
 
 require LSpec from git
-  "https://github.com/lurk-lab/LSpec" @ "3b6023654b917c8641ec5e626724a43380cff8f0"
+  "https://github.com/lurk-lab/LSpec" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 
 require YatimaStdLib from git
-  "https://github.com/lurk-lab/YatimaStdLib.lean" @ "5b64c5150e371fb280728cbb5b7c225b9c96b348"
+  "https://github.com/lurk-lab/YatimaStdLib.lean" @ "3037f0c14128751b95510c2723f067ec7a494f08"
 
 require Straume from git
-  "https://github.com/lurk-lab/straume" @ "053d9feccbface9a0b2c1a72447914376aac74ea"
+  "https://github.com/lurk-lab/straume" @ "ad2aa666b7e4148df450ecf74aedb477f1535534"
 
 @[default_target]
 lean_exe megaparsec {
diff --git a/lean-toolchain b/lean-toolchain
index f0a6d66..26638e0 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.4.0