lake update - run after updating the lean version

Paper-Proof · Sep 29, 2024 · f5f6fc5 · f5f6fc5
1 parent 8e226f1
commit f5f6fc5
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 12 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,7 +1,8 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",
+   "scope": "",
    "name": "Paperproof",
    "manifestFile": "lake-manifest.json",
    "inherited": false,
@@ -10,7 +11,8 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "cac5bff36ff3c339d8fdb0d1506ec789ce57a6fd",
+   "scope": "leanprover-community",
+   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -19,7 +21,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -28,7 +31,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "093226b2a8c0cdeac12f1b4786827c67c673b4fb",
+   "scope": "leanprover-community",
+   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -37,34 +41,48 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "e9fb4ecc5d718eb36faae5308880cd3f243788df",
+   "scope": "leanprover-community",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "ad584cd896933c986cdf1ab29436c675705ffca1",
+   "scope": "",
+   "rev": "301f54abf16c4d7706fb65a94ece16e384d6622e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json
@@ -1 +1,5 @@
-{"version": 5, "packagesDir": "lake-packages", "packages": []}
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "Paperproof",
+ "lakeDir": ".lake"}