From 8eb7eaaee796379e29e7202f5a90320828d43f4d Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Dec 2024 19:23:12 +0100 Subject: [PATCH] chore: update to nightly-testing-2024-12-25 (#915) --- 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 8060d2c2a..6a2b06f3d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ed546d89ba3b9fa2c93b3501b9f6aac3593c930d", + "rev": "8157db740f7cbf298fb4839f6b1b81b03f76d44e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-23", + "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": "6b16a9378726331e9f4b1a044dbda82261b2cfef", + "rev": "7f9e7a655e6602b674657a3be7eabcf84c905446", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 71f519add..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-23" +rev = "nightly-testing-2024-12-25" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index c0d8a978e..62b3dc2fb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-23 +leanprover/lean4:nightly-2024-12-25