diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index b5b36c2..f312e5a 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -1,95 +1,95 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.14.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d", - "name": "batteries", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", - "name": "Qq", + "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b", - "name": "aesop", + "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1383e72b40dd62a566896a6e348ffe868801b172", + "rev": "68280daef58803f68368eb2e53046dabcd270c9d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.46", + "inputRev": "v0.0.47", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", - "name": "Cli", + "scope": "leanprover-community", + "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ac7b989cbf99169509433124ae484318e953d201", - "name": "importGraph", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7bedaed1ef024add1e171cc17706b012a9a37802", - "name": "LeanSearchClient", + "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e", - "name": "plausible", + "scope": "leanprover", + "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", + "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a7fc949f1b05c2a01e01c027fd9f480496a1253e", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0-rc1", - "inherited": false, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.toml"}], "name": "«repl-mathlib-tests»", "lakeDir": ".lake"} diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index 1e70935..401bc14 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.14.0 \ No newline at end of file