From 5db65f542f0203a4d60c3d7a7b445378478ec62a Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Dec 2024 17:50:06 +0100 Subject: [PATCH] chore: update to nightly-testing-2024-12-25 --- lake-manifest.json | 8 ++++---- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) 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