From 8d5321626222f7e4f77cb8f0ad9b60a85843a809 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Mon, 19 Feb 2024 11:40:31 -0300
Subject: [PATCH] Revert "chore: Update lean-toolchain to 4.4.0"

---
 .gitignore         |  1 -
 lake-manifest.json | 51 ++++++++++++++++++----------------------------
 lakefile.lean      |  4 ++--
 lean-toolchain     |  2 +-
 4 files changed, 23 insertions(+), 35 deletions(-)

diff --git a/.gitignore b/.gitignore
index d571524..2ee099a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,2 @@
 /build
 /lake-packages
-.lake
diff --git a/lake-manifest.json b/lake-manifest.json
index 9d9c212..394add0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,32 +1,21 @@
-{"version": 7,
- "packagesDir": ".lake/packages",
+{"version": 4,
+ "packagesDir": "./lake-packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4/",
-   "type": "git",
-   "subDir": null,
-   "rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
-   "name": "std",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.4.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/lurk-lab/LSpec",
-   "type": "git",
-   "subDir": null,
-   "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
-   "name": "LSpec",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
-   "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"}],
- "name": "Cli",
- "lakeDir": ".lake"}
+ [{"git":
+   {"url": "https://github.com/lurk-lab/YatimaStdLib.lean",
+    "subDir?": null,
+    "rev": "649368d593f292227ab39b9fd08f6a448770dca8",
+    "name": "YatimaStdLib",
+    "inputRev?": "649368d593f292227ab39b9fd08f6a448770dca8"}},
+  {"git":
+   {"url": "https://github.com/yatima-inc/lspec/",
+    "subDir?": null,
+    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "name": "LSpec",
+    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4/",
+    "subDir?": null,
+    "rev": "fde95b16907bf38ea3f310af406868fc6bcf48d1",
+    "name": "std",
+    "inputRev?": "fde95b16907bf38ea3f310af406868fc6bcf48d1"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index 31bbf52..d1abee3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,7 +7,7 @@ package Cli
 lean_lib Cli
 
 require std from git
-  "https://github.com/leanprover/std4/" @ "v4.4.0"
+  "https://github.com/leanprover/std4/" @ "fde95b16907bf38ea3f310af406868fc6bcf48d1"
 
 require YatimaStdLib from git
-  "https://github.com/lurk-lab/YatimaStdLib.lean" @ "3037f0c14128751b95510c2723f067ec7a494f08"
+  "https://github.com/lurk-lab/YatimaStdLib.lean" @ "649368d593f292227ab39b9fd08f6a448770dca8"
diff --git a/lean-toolchain b/lean-toolchain
index 7638861..b20d041 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:stable
+leanprover/lean4:nightly-2023-01-10