update lean/mathlib

mo271 · Aug 1, 2023 · 979b920 · 979b920
1 parent 7f036bc
commit 979b920
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 16 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -2,32 +2,38 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
-    "subDir?": null,
-    "rev": "d9d26c4ff7e421f56246bc8c5e2187cea4f7b2ab",
-    "name": "mathlib",
-    "inputRev?": null}},
-   {"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
     "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
-      {"git":
+    "inputRev?": "v0.0.13"}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "name": "Cli",
+    "inputRev?": "nightly"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4",
+    "subDir?": null,
+    "rev": "6c5ad83c2ca4a6e03ae9e33fa52220712b8a9faf",
+    "name": "mathlib",
+    "inputRev?": "6c5ad83c2ca4a6e03ae9e33fa52220712b8a9faf"}},
+  {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
+    "rev": "354432d437fb37738ed93ac6988669d78a870ed0",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936",
+    "rev": "e3c2be331da9ddeef7f82ca363f072a68d7210b3",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lakefile.lean b/lakefile.lean
@@ -5,11 +5,10 @@ package formal_book {
   -- add any package configuration options here
 }
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
 
 @[default_target]
 lean_lib «FormalBook» {
   -- add any library configuration options here
 }
+
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "6c5ad83c2ca4a6e03ae9e33fa52220712b8a9faf"
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-06-20
+leanprover/lean4:nightly-2023-07-30