chore: Use Lean v4.4.0

argumentcomputer · Dec 25, 2023 · ff58040 · ff58040
1 parent 33509a4
commit ff58040
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 24 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,2 +1,3 @@
 /build
 /lake-packages
+/.lake
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,21 +1,32 @@
-{"version": 4,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/lurk-lab/YatimaStdLib.lean",
-    "subDir?": null,
-    "rev": "974c288349a412aea92bb0780efc81fa5f79e442",
-    "name": "YatimaStdLib",
-    "inputRev?": "974c288349a412aea92bb0780efc81fa5f79e442"}},
-  {"git":
-   {"url": "https://github.com/lurk-lab/LSpec",
-    "subDir?": null,
-    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "name": "LSpec",
-    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41"}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
-    "name": "std",
-    "inputRev?": "6006307d2ceb8743fea7e00ba0036af8654d0347"}}]}
+ [{"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": false,
+   "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": "Straume",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -6,13 +6,13 @@ package Straume
 lean_lib Straume
 
 require std from git
-  "https://github.com/leanprover/std4" @ "6006307d2ceb8743fea7e00ba0036af8654d0347"
+  "https://github.com/leanprover/std4" @ "v4.4.0"
 
 require LSpec from git
-  "https://github.com/lurk-lab/LSpec" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+  "https://github.com/lurk-lab/LSpec" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 
 require YatimaStdLib from git
-  "https://github.com/lurk-lab/YatimaStdLib.lean" @ "974c288349a412aea92bb0780efc81fa5f79e442"
+  "https://github.com/lurk-lab/YatimaStdLib.lean" @ "3037f0c14128751b95510c2723f067ec7a494f08"
 
 @[default_target]
 lean_exe straume where

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-06
+leanprover/lean4:v4.4.0
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2023-05-06
		leanprover/lean4:v4.4.0