From 51e8e24db7b41dd848db7339697f6261a5caa002 Mon Sep 17 00:00:00 2001 From: Joscha Date: Tue, 26 May 2026 22:48:50 +0200 Subject: [PATCH] chore: bump toolchain to v4.30.0 --- lean-toolchain | 2 +- test/Mathlib/lake-manifest.json | 28 ++++++++++++++-------------- test/Mathlib/lakefile.toml | 2 +- test/Mathlib/lean-toolchain | 2 +- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/lean-toolchain b/lean-toolchain index 6c7e31ff..af9e5d33 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.30.0 diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index d943874b..ed9c558b 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", + "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", + "rev": "a456461b368b71d2accd95234832cd9c174b5437", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,50 +45,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", + "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.98", + "inputRev": "v0.0.99", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", + "rev": "558915ae105bfd8074e22d597613d1961822adc2", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "«repl-mathlib-tests»", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index ebc85ea7..bd22de40 100644 --- a/test/Mathlib/lakefile.toml +++ b/test/Mathlib/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "v4.30.0-rc2" +rev = "v4.30.0" [[lean_lib]] name = "ReplMathlibTests" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index 6c7e31ff..af9e5d33 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.30.0