From 42b1d0308d50a5d3f1322e3b3c9d2c1e54358ea4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 4 Jan 2025 16:20:20 +1100 Subject: [PATCH 1/2] chore: bump toolchain to v4.16.0-rc1 --- lakefile.toml | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.toml b/lakefile.toml index 6534e63..3aaa8a5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -14,7 +14,7 @@ rev = "main" [[require]] name = "batteries" scope = "leanprover-community" -rev = "v4.15.0" +rev = "v4.16.0-rc1" [[lean_lib]] name = "ImportGraph" diff --git a/lean-toolchain b/lean-toolchain index d0eb99f..62ccd71 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.16.0-rc1 From eda37c9bda186b5ea28b4681b38f65fcf5dfe163 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 4 Jan 2025 16:20:52 +1100 Subject: [PATCH 2/2] lake update --- lake-manifest.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 5652ef7..0d23030 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli",