Align optional packages with Lean 4.34.0

Upgrade Mathlib and Verso and refresh their dependency manifests. Remove the unused metatheory umbrella module and import Soundness directly in its integration test.

Author: AD1024

Crush/Metatheory.lean

@@ -12,17 +12,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e09d21a5f7f66c9fc985b73197708298569bf583",
+   "rev": "cad4b633e75ea769b851f12f9ca3b4f0dfcc625f",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b3debfe6b629192033ef87257e1c60201881646f",
+   "rev": "a1a61c9678da010e958ed24cdfa6f635b85f172a",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -32,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
+   "rev": "9b90b7f938d6169246325df002351014f49945ef",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

Doc/Verso/lake-manifest.json

@@ -9,7 +9,7 @@ package «crush-docs» where
     ⟨`linter.unusedVariables, false⟩
   ]
 
-require "leanprover" / verso @ git "v4.32.0"
+require "leanprover" / verso @ git "v4.34.0"
 
 require crush from "../.."
 

Doc/Verso/lakefile.lean

@@ -1 +1 @@
-leanprover/lean4:v4.32.2
+leanprover/lean4:v4.34.0

Doc/Verso/lean-toolchain

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "905b95818eb32af7874a58b427f50c1711a5e96c",
+   "rev": "5ed2965256430c3649e86755f9576b54eca72435",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.2",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
@@ -22,7 +22,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
+   "rev": "e928b72544873815af278d38681b31c0293588e3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
+   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
+   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -72,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
+   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,10 +92,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0",
+   "inputRev": "v4.34.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "crushMathlibTest",

MathlibTest/lake-manifest.json

@@ -4,7 +4,7 @@ open Lake DSL
 -- Mathlib integration tests are a separate package so installing `crush` does not
 -- fetch Mathlib or its transitive dependency graph.
 require crush from ".."
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.2"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.34.0"
 
 package crushMathlibTest where
   reservoir := false

MathlibTest/lakefile.lean

@@ -1 +1 @@
-leanprover/lean4:v4.32.2
+leanprover/lean4:v4.34.0

MathlibTest/lean-toolchain

@@ -1,4 +1,4 @@
-import Crush.Metatheory
+import Crush.Metatheory.Soundness
 
 open scoped Crush.Metatheory