diff --git a/lake-manifest.json b/lake-manifest.json index c47dfee4e..6a2b06f3d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9a6b101b298066238b15e3fbd66618c2088cc693", + "rev": "8157db740f7cbf298fb4839f6b1b81b03f76d44e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-24", + "inputRev": "nightly-testing-2024-12-25", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "03373e3b951d03e216837a5b14f28b5ab9664a98", + "rev": "7f9e7a655e6602b674657a3be7eabcf84c905446", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index c4c99cf44..6b61ec9ce 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-24" +rev = "nightly-testing-2024-12-25" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 6f7dca929..62b3dc2fb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-24 +leanprover/lean4:nightly-2024-12-25