From e8e00100077554acfda66372f845cd94e247beb3 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Fri, 15 Aug 2025 18:46:57 +0000 Subject: [PATCH 01/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/9932 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 16b0dc8f4797b7..0b4e5ad08dbc34 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b96d0a767dcdf49d1a84dccdd827ad163efecf9a", + "rev": "18112711593e15c6e549deffc6d0579d7cb653ab", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-9932", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index f58c69512f66c2..c5455b10e14546 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-9932" require "leanprover-community" / "Qq" @ git "master" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.68" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index 71f6e8fce5fb06..35d0acf760edcf 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-08-14 +leanprover/lean4-pr-releases:pr-release-9932-9a14caf From a0325485003318269c5eeb6c0b7dabce5181b136 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 23 Sep 2025 16:18:57 +0000 Subject: [PATCH 02/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/10319 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e34f38ecaea9ed..6beb8d23c78a40 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "15a1cfc8b9e8191e67ebeaf5a6adf8abff3ab742", + "rev": "0da43cc2c61cc9ad2cae9ace5edfc1ee594a7a24", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-10319", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 5393405124a01b..26e44184e060dd 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-10319" require "leanprover-community" / "Qq" @ git "master" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre2" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index 15674d2056415c..3b9e77af44aab1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-21 +leanprover/lean4-pr-releases:pr-release-10319-82093dc From 8e3e8b7a8cb62b097637ba219c6f9bf4f4fb38f8 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 24 Sep 2025 07:45:36 +0000 Subject: [PATCH 03/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/10319 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 6beb8d23c78a40..914544d41b7f59 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0da43cc2c61cc9ad2cae9ace5edfc1ee594a7a24", + "rev": "9594262a30b61e5741666dc14f92ef150ae10914", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10319", diff --git a/lean-toolchain b/lean-toolchain index 3b9e77af44aab1..5bc46ddd2cfa22 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-10319-82093dc +leanprover/lean4-pr-releases:pr-release-10319-9b16825 From f2d994c9ac27207ea6b24fda9d81d9182978239d Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 24 Sep 2025 10:32:57 +0200 Subject: [PATCH 04/77] update LibraryRewrite.lean --- MathlibTest/LibraryRewrite.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/MathlibTest/LibraryRewrite.lean b/MathlibTest/LibraryRewrite.lean index 797579674e62c6..0d8215797dc4fb 100644 --- a/MathlibTest/LibraryRewrite.lean +++ b/MathlibTest/LibraryRewrite.lean @@ -86,6 +86,8 @@ info: Pattern n + 1 Std.PRange.Nat.succ_eq · (↑n + 1).toNat Int.toNat_natCast_add_one +· (*...=n).size + Std.PRange.Nat.size_Ric Pattern n + m · 1 + n From 249cb40066044ea556e473e0be7b98d07a75d891 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 24 Sep 2025 09:18:11 +0000 Subject: [PATCH 05/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/10319 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 914544d41b7f59..5654d2f9743e86 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9594262a30b61e5741666dc14f92ef150ae10914", + "rev": "34276b86455d294defa78248a76234ed543330ab", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10319", diff --git a/lean-toolchain b/lean-toolchain index 5bc46ddd2cfa22..ddfee4c634ac13 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-10319-9b16825 +leanprover/lean4-pr-releases:pr-release-10319-167265f From 65544a51451343c1d8ff5a8fd44350c6a4469d88 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 24 Sep 2025 14:32:03 +0200 Subject: [PATCH 06/77] really fix LibraryRewrite --- MathlibTest/LibraryRewrite.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/MathlibTest/LibraryRewrite.lean b/MathlibTest/LibraryRewrite.lean index 0d8215797dc4fb..ee05ee645f41bf 100644 --- a/MathlibTest/LibraryRewrite.lean +++ b/MathlibTest/LibraryRewrite.lean @@ -84,10 +84,10 @@ info: Pattern n + 1 Nat.add_one · Std.PRange.succ n Std.PRange.Nat.succ_eq -· (↑n + 1).toNat - Int.toNat_natCast_add_one · (*...=n).size Std.PRange.Nat.size_Ric +· (↑n + 1).toNat + Int.toNat_natCast_add_one Pattern n + m · 1 + n From ff15f33d1b36c44b76b64cfb84d9cd60f15ff066 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 24 Sep 2025 16:41:01 +0000 Subject: [PATCH 07/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/10319 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 5654d2f9743e86..92e53409312c46 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "34276b86455d294defa78248a76234ed543330ab", + "rev": "d01be8e68d72fa83658dd621e66c5fba4f8e85e0", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10319", diff --git a/lean-toolchain b/lean-toolchain index ddfee4c634ac13..3dd54261862205 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-10319-167265f +leanprover/lean4-pr-releases:pr-release-10319-73b1991 From 6a44211b1ce7044527986389f3f75b53e6688764 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 24 Sep 2025 22:40:59 +0200 Subject: [PATCH 08/77] shake --- Mathlib/SetTheory/PGame/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/SetTheory/PGame/Basic.lean b/Mathlib/SetTheory/PGame/Basic.lean index 4e9d1489f7f67a..121ac31f2267c8 100644 --- a/Mathlib/SetTheory/PGame/Basic.lean +++ b/Mathlib/SetTheory/PGame/Basic.lean @@ -3,7 +3,6 @@ Copyright (c) 2019 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Kim Morrison, Yuyang Zhao -/ -import Mathlib.Data.Nat.Basic import Mathlib.Logic.Equiv.Defs import Mathlib.Tactic.Convert import Mathlib.Tactic.Linter.DeprecatedModule From c4f744554a9f8ae3669d5c2a56dad6a2a3d290a1 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 25 Sep 2025 09:14:41 +0000 Subject: [PATCH 09/77] chore: bump to nightly-2025-09-25 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 23b82c71992403..5ab4786210f6d8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-24 +leanprover/lean4:nightly-2025-09-25 From 8b8f01b415a9a82c6f8ef8c28ebcff5f6dae65df Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 25 Sep 2025 12:38:22 +0200 Subject: [PATCH 10/77] update batteries --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index fcc6265a308bab..8a64f780934a1e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23aa881d96613ebccacbd345d4fbf5be4d06a871", + "rev": "2f914316e28b9568a42b68cba7982b4ae2682206", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From c0abbc516aa784925f153212250aaed696227658 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 25 Sep 2025 12:38:51 +0200 Subject: [PATCH 11/77] remove upstreamed --- Mathlib/Data/String/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean index 8273444d78aeff..d70c1463bf3a03 100644 --- a/Mathlib/Data/String/Basic.lean +++ b/Mathlib/Data/String/Basic.lean @@ -16,8 +16,6 @@ Supplementary theorems about the `String` type. namespace String -@[simp] theorem endPos_empty : "".endPos = 0 := rfl - /-- `<` on string iterators. This coincides with `<` on strings as lists. -/ def ltb (s₁ s₂ : Iterator) : Bool := if s₂.hasNext then From 0535eef8719b8d911c143530ce7228be4948f21b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 25 Sep 2025 13:12:55 +0200 Subject: [PATCH 12/77] update Qq --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 8a64f780934a1e..cca6eafd1215a8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7032fae8ca26da4982852b813f2af6c1dcd9d1cc", + "rev": "b255307f0a1f721b999332e3be14a60b1d82af12", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From cc0437aba0f38a81d2cb130a5083ed17badc8206 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 25 Sep 2025 22:46:19 +0000 Subject: [PATCH 13/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/10188 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b720e410359e31..26cddf5df64f84 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "981747b59c23164db11bb87ac9918c8154d82f9c", + "rev": "9e312ca41ad9176f3cd0f27cca298e9f7afab03c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-10188", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 5393405124a01b..e7fc96e6e76b31 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-10188" require "leanprover-community" / "Qq" @ git "master" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre2" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index f6c41bdce79773..366c273b019a62 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-22 +leanprover/lean4-pr-releases:pr-release-10188-9dee752 From fddb49791fb4b5e4a1e29fed393cc2923b1818e8 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 22 Sep 2025 22:24:27 +0200 Subject: [PATCH 14/77] fix(Cache): use leantar v0.1.16-pre2 --- Cache/IO.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cache/IO.lean b/Cache/IO.lean index f71f718751fd68..530959bda78bbb 100644 --- a/Cache/IO.lean +++ b/Cache/IO.lean @@ -70,7 +70,7 @@ def CURLBIN := /-- leantar version at https://github.com/digama0/leangz -/ def LEANTARVERSION := - "0.1.15" + "0.1.16-pre2" def EXE := if System.Platform.isWindows then ".exe" else "" From 6ad0b9e77b3bbe677c4898dfeb475ad7a64f33a5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 26 Sep 2025 06:01:38 +0200 Subject: [PATCH 15/77] attempt to fix cache --- Cache/IO.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Cache/IO.lean b/Cache/IO.lean index 530959bda78bbb..64908ca2ae05f7 100644 --- a/Cache/IO.lean +++ b/Cache/IO.lean @@ -317,6 +317,11 @@ def mkBuildPaths (mod : Name) : CacheM <| List (FilePath × Bool) := do (packageDir / LIBDIR / path.withExtension "ilean.hash", true), (packageDir / IRDIR / path.withExtension "c", true), (packageDir / IRDIR / path.withExtension "c.hash", true), + -- this is needed for packages using the module system: + (packageDir / LIBDIR / path.withExtension "olean.private", false), + (packageDir / LIBDIR / path.withExtension "olean.private.hash", false), + (packageDir / LIBDIR / path.withExtension "olean.server", false), + (packageDir / LIBDIR / path.withExtension "olean.server.hash", false), (packageDir / LIBDIR / path.withExtension "extra", false)] /-- Check that all required build files exist. -/ From 19120fefc79dcb7149b8de1df0bdd8e55e906622 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 26 Sep 2025 06:51:21 +0200 Subject: [PATCH 16/77] whitespace to invalidate cache --- lakefile.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/lakefile.lean b/lakefile.lean index aaf5b6466819ff..ce527e0977a981 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -18,6 +18,7 @@ require "leanprover-community" / "importGraph" @ git "nightly-testing" require "leanprover-community" / "LeanSearchClient" @ git "main" require "leanprover-community" / "plausible" @ git "main" + /-! ## Options for building mathlib -/ From c609f29249b320f1a7e099f65f18b175be1b0792 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Fri, 26 Sep 2025 10:52:58 +0000 Subject: [PATCH 17/77] chore: bump to nightly-2025-09-26 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 5ab4786210f6d8..0be5608acb1b7a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-25 +leanprover/lean4:nightly-2025-09-26 From 2120cf6d1f009ef4225ac5a353d0123dd16ead2b Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sun, 28 Sep 2025 09:38:20 +0000 Subject: [PATCH 18/77] chore: bump to nightly-2025-09-28 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 0be5608acb1b7a..a4a6e8ee1c20b5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-26 +leanprover/lean4:nightly-2025-09-28 From 607a551a4a65f2c5b14c6d7e15a5ffe3f523c04b Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 29 Sep 2025 09:03:19 +0000 Subject: [PATCH 19/77] chore: bump to nightly-2025-09-29 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index a4a6e8ee1c20b5..08b0beb355db7d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-28 +leanprover/lean4:nightly-2025-09-29 From 196f322896d57c562f24f8911a10c6ae7932d936 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 29 Sep 2025 15:16:09 +0000 Subject: [PATCH 20/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/9932 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 2fd96f09f3728a..b15b1ff575d6e3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "89fc732af7d61c9feb01cabf0b0a7d32c616169f", + "rev": "ddc76a90c8a102772bf075dea8342de4e984f1de", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-9932", diff --git a/lean-toolchain b/lean-toolchain index 0ec060e9ef04c6..6d77bf1f82c977 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-9932-5fca174 +leanprover/lean4-pr-releases:pr-release-9932-1c79aac From 9c3bb427fa8f3d8daca22183a4bdb68eb6b2b2c7 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 30 Sep 2025 08:46:05 +0200 Subject: [PATCH 21/77] Fix --- Mathlib/Data/Int/LeastGreatest.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Int/LeastGreatest.lean b/Mathlib/Data/Int/LeastGreatest.lean index 97c9aedb514494..d3909431cdbd70 100644 --- a/Mathlib/Data/Int/LeastGreatest.lean +++ b/Mathlib/Data/Int/LeastGreatest.lean @@ -75,7 +75,11 @@ theorem exists_least_of_bdd theorem coe_leastOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z) (Hb' : ∀ z : ℤ, P z → b' ≤ z) (Hinh : ∃ z : ℤ, P z) : (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh := by - grind + #adaptation_note /-- 2025-09-30 (https://github.com/leanprover/lean4/issues/10622) + Used to be `grind` -/ + rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩ + rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩ + exact le_antisymm (h2n _ hn') (h2n' _ hn) /-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the integers, with an explicit upper bound and a proof that it is somewhere true, return @@ -112,6 +116,10 @@ theorem exists_greatest_of_bdd theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → z ≤ b) (Hb' : ∀ z : ℤ, P z → z ≤ b') (Hinh : ∃ z : ℤ, P z) : (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh := by - grind + #adaptation_note /-- 2025-09-30 (https://github.com/leanprover/lean4/issues/10622) + Used to be `grind` -/ + rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩ + rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩ + exact le_antisymm (h2n' _ hn) (h2n _ hn') end Int From 791bc4685b99033d3d2336c8caa27145f8a84f5b Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 30 Sep 2025 10:06:25 +0200 Subject: [PATCH 22/77] Fix --- .../IntervalIntegral/LebesgueDifferentiationThm.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean index 5e46167ecc7348..f7ee3b57b3421a 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean @@ -70,7 +70,10 @@ theorem IntervalIntegrable.ae_hasDerivAt_integral {f : ℝ → ℝ} {a b : ℝ} |>.integrable_of_forall_notMem_eq_zero (by grind) |>.locallyIntegrable filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hg, h₁, h₂] with x hx _ _ _ intro c hc - refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <| Ioo_mem_nhds (by grind) (by grind) - rw [show f x = g x by grind] + #adaptation_note /-- 2025-09-30 https://github.com/leanprover/lean4/issues/10622 + `grind -order` calls used be `grind` -/ + refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <| + Ioo_mem_nhds (by grind -order) (by grind -order) + rw [show f x = g x by grind -order] refine (hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_ all_goals apply intervalIntegral.integral_congr_ae' <;> filter_upwards <;> grind From dbf4d25a13c45774a85bbe68777a7d0692542bc1 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 30 Sep 2025 08:49:26 +0000 Subject: [PATCH 23/77] chore: bump to nightly-2025-09-30 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 08b0beb355db7d..1be8b1fbd7f8c6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-29 +leanprover/lean4:nightly-2025-09-30 From c5b4287e9750db1c1c9192af833bb3d0aa5997fd Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 30 Sep 2025 13:15:39 +0200 Subject: [PATCH 24/77] Pin Qq for now --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index ce527e0977a981..a9a31f8a7951a6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ open Lake DSL -/ require "leanprover-community" / "batteries" @ git "nightly-testing" -require "leanprover-community" / "Qq" @ git "nightly-testing" +require "leanprover-community" / "Qq" @ git "7032fae8ca26da4982852b813f2af6c1dcd9d1cc" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre2" -- ProofWidgets should always be pinned to a specific version with NameMap.empty.insert `errorOnBuild From 198396395e97a5b5ef21ab49d14f442b4e9b6075 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 30 Sep 2025 14:13:54 +0200 Subject: [PATCH 25/77] Unpin Qq again This reverts commit c5b4287e9750db1c1c9192af833bb3d0aa5997fd. --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index a9a31f8a7951a6..ce527e0977a981 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ open Lake DSL -/ require "leanprover-community" / "batteries" @ git "nightly-testing" -require "leanprover-community" / "Qq" @ git "7032fae8ca26da4982852b813f2af6c1dcd9d1cc" +require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre2" -- ProofWidgets should always be pinned to a specific version with NameMap.empty.insert `errorOnBuild From 4dc7275b99d5913fe52e8fc73620403e27668fb5 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 30 Sep 2025 14:15:42 +0200 Subject: [PATCH 26/77] lake update --- lake-manifest.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0548b5d0830dd9..9e30f090a48128 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b255307f0a1f721b999332e3be14a60b1d82af12", + "rev": "ba88b081e2bea3981d4ff227d1e0d877661d7c76", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4971c6b8224745396030f7668717a9f55b566d83", + "rev": "3113710fe9deb50768c66112bde68cceee6b3c83", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From 7ec524ff29ebcf2708770ddf4d8d37f84a27e149 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 30 Sep 2025 16:20:55 +0200 Subject: [PATCH 27/77] Fix --- Mathlib/Algebra/Algebra/StrictPositivity.lean | 2 +- .../ContinuousFunctionalCalculus/ExpLog.lean | 6 +++--- .../ContinuousFunctionalCalculus/Rpow/Basic.lean | 6 +++--- MathlibTest/FindSyntax.lean | 12 ++++++------ MathlibTest/Simps.lean | 2 +- MathlibTest/Util/PrintSorries.lean | 16 ++++++---------- 6 files changed, 20 insertions(+), 24 deletions(-) diff --git a/Mathlib/Algebra/Algebra/StrictPositivity.lean b/Mathlib/Algebra/Algebra/StrictPositivity.lean index 51e62d7b3171b4..9f036a5eac5dc9 100644 --- a/Mathlib/Algebra/Algebra/StrictPositivity.lean +++ b/Mathlib/Algebra/Algebra/StrictPositivity.lean @@ -60,7 +60,7 @@ lemma _root_.IsUnit.isStrictlyPositive [LE A] [Monoid A] [Zero A] lemma isSelfAdjoint [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A} (ha : IsStrictlyPositive a) : IsSelfAdjoint a := ha.nonneg.isSelfAdjoint -@[simp, grind] +@[simp, grind .] lemma _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] : IsStrictlyPositive (1 : A) := iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩ diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean index bca911abbf022d..15ee863e97475d 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean @@ -115,12 +115,12 @@ variable {A : Type*} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] matrices, operators on a Hilbert space, elements of a C⋆-algebra, etc. -/ noncomputable def log (a : A) : A := cfc Real.log a -@[simp, grind] +@[simp, grind =>] protected lemma _root_.IsSelfAdjoint.log {a : A} : IsSelfAdjoint (log a) := cfc_predicate _ a -@[simp, grind] lemma log_zero : log (0 : A) = 0 := by simp [log] +@[simp, grind =] lemma log_zero : log (0 : A) = 0 := by simp [log] -@[simp, grind] lemma log_one : log (1 : A) = 0 := by simp [log] +@[simp, grind =] lemma log_one : log (1 : A) = 0 := by simp [log] @[simp, grind =] lemma log_algebraMap {r : ℝ} : log (algebraMap ℝ A r) = algebraMap ℝ A (Real.log r) := by diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean index fc556a3d9c9498..6abe9a22a853e8 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean @@ -93,7 +93,7 @@ noncomputable instance (priority := 100) : Pow A ℝ≥0 where @[simp] lemma nnrpow_eq_pow {a : A} {y : ℝ≥0} : nnrpow a y = a ^ y := rfl -@[simp, grind] +@[simp, grind =>] lemma nnrpow_nonneg {a : A} {x : ℝ≥0} : 0 ≤ a ^ x := cfcₙ_predicate _ a lemma nnrpow_def {a : A} {y : ℝ≥0} : a ^ y = cfcₙ (NNReal.nnrpow · y) a := rfl @@ -226,7 +226,7 @@ section sqrt /-- Square roots of operators, based on the non-unital continuous functional calculus. -/ noncomputable def sqrt (a : A) : A := cfcₙ NNReal.sqrt a -@[simp, grind] +@[simp, grind =>] lemma sqrt_nonneg (a : A) : 0 ≤ sqrt a := cfcₙ_predicate _ a lemma sqrt_eq_nnrpow (a : A) : sqrt a = a ^ (1 / 2 : ℝ≥0) := by @@ -381,7 +381,7 @@ noncomputable instance (priority := 100) : Pow A ℝ where @[simp] lemma rpow_eq_pow {a : A} {y : ℝ} : rpow a y = a ^ y := rfl -@[simp, grind] +@[simp, grind =>] lemma rpow_nonneg {a : A} {y : ℝ} : 0 ≤ a ^ y := cfc_predicate _ a lemma rpow_def {a : A} {y : ℝ} : a ^ y = cfc (fun x : ℝ≥0 => x ^ y) a := rfl diff --git a/MathlibTest/FindSyntax.lean b/MathlibTest/FindSyntax.lean index 6559273db8dd08..48e3fcd3877502 100644 --- a/MathlibTest/FindSyntax.lean +++ b/MathlibTest/FindSyntax.lean @@ -3,7 +3,7 @@ import Mathlib.Tactic.FindSyntax infix:65 " #find_syntax_add " => Nat.add /-- -info: Found 2 uses among over 700 syntax declarations +info: Found 2 uses among over 800 syntax declarations In `MathlibTest.FindSyntax`: «term_#find_syntax_add_»: '#find_syntax_add' @@ -14,7 +14,7 @@ In `Mathlib.Tactic.FindSyntax`: #find_syntax "#find_syntax" approx -- an `infix` in two files, one being the current one /-- -info: Found 1 use among over 700 syntax declarations +info: Found 1 use among over 800 syntax declarations In `Init.Notation`: «term_∘_»: '∘' -/ @@ -22,7 +22,7 @@ In `Init.Notation`: #find_syntax "∘" approx -- an `infixr` /-- -info: Found 1 use among over 700 syntax declarations +info: Found 1 use among over 800 syntax declarations In `Init.Notation`: «term_∣_»: '∣' -/ @@ -30,7 +30,7 @@ In `Init.Notation`: #find_syntax "∣" approx -- an `infix` /-- -info: Found 2 uses among over 700 syntax declarations +info: Found 2 uses among over 800 syntax declarations In `Init.Notation`: «stx_,*»: ',*' «stx_,*,?»: ',*,?' @@ -39,7 +39,7 @@ In `Init.Notation`: #find_syntax ",*" approx -- generated by a `macro` /-- -info: Found 1 use among over 700 syntax declarations +info: Found 1 use among over 800 syntax declarations In `Init.Notation`: «term~~~_»: '~~~' -/ @@ -47,7 +47,7 @@ In `Init.Notation`: #find_syntax "~~~" approx -- a `prefix` /-- -info: Found 15 uses among over 700 syntax declarations +info: Found 15 uses among over 800 syntax declarations In `Init.Tactics`: Lean.Parser.Tactic.mrefineMacro: 'mrefine' Lean.Parser.Tactic.refine: 'refine' diff --git a/MathlibTest/Simps.lean b/MathlibTest/Simps.lean index 4f9fde0b179983..4228d50d4365e6 100644 --- a/MathlibTest/Simps.lean +++ b/MathlibTest/Simps.lean @@ -1269,7 +1269,7 @@ end UnderScoreDigit namespace Grind -@[simps (attr := grind) -isSimp] +@[simps (attr := grind =) -isSimp] def foo := (2, 3) example : foo.1 = 2 := by grind diff --git a/MathlibTest/Util/PrintSorries.lean b/MathlibTest/Util/PrintSorries.lean index 0c3697d4109d34..1d39a7241355c6 100644 --- a/MathlibTest/Util/PrintSorries.lean +++ b/MathlibTest/Util/PrintSorries.lean @@ -193,26 +193,22 @@ warning: declaration uses 'sorry' Check that `admit` and `stop` are correctly handled -/ -/-- info: thm4 has sorry of type +/-- +info: thm4 has sorry of type True --- warning: declaration uses 'sorry' ---- -warning: 'admit' tactic does nothing - -Note: This linter can be disabled with `set_option linter.unusedTactic false` -/ +-/ #guard_msgs in #print sorries in theorem thm4 : True := by admit -/-- info: thm5 has sorry of type +/-- +info: thm5 has sorry of type True --- warning: declaration uses 'sorry' ---- -warning: 'stop admit' tactic does nothing - -Note: This linter can be disabled with `set_option linter.unusedTactic false` -/ +-/ #guard_msgs in #print sorries in theorem thm5 : True := by stop admit From 2dafcfc901385d3970b2fd701871cea0533b785d Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 30 Sep 2025 14:56:07 +0000 Subject: [PATCH 28/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/10624 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 9e30f090a48128..bd697aa82a5ea2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3113710fe9deb50768c66112bde68cceee6b3c83", + "rev": "0f4e5cddb8a79b9a3c7be10fcd683db1b3ec460e", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-10624", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index ce527e0977a981..ff7e6397705a08 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-10624" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre2" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index 1be8b1fbd7f8c6..1aa4bac47a1a4c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-30 +leanprover/lean4-pr-releases:pr-release-10624-0619264 From 443cb101c58f19ce66e8c96fd1f1c3124a9811f7 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 1 Oct 2025 07:59:30 +0200 Subject: [PATCH 29/77] Lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index bd697aa82a5ea2..6e135ffaf2690a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0f4e5cddb8a79b9a3c7be10fcd683db1b3ec460e", + "rev": "f95888dbf93c254740b54469c6b7cab70a806832", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10624", From 6d02d76a9d5970e1d9a14fa16d801f973d65c12b Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Oct 2025 07:25:45 +0000 Subject: [PATCH 30/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/9932 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b15b1ff575d6e3..8910665620157f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ddc76a90c8a102772bf075dea8342de4e984f1de", + "rev": "e5f27d9c0b8d8e846d6e3b0d3ce605e63122827d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-9932", diff --git a/lean-toolchain b/lean-toolchain index 6d77bf1f82c977..b211b210a4d15e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-9932-1c79aac +leanprover/lean4-pr-releases:pr-release-9932-ab30cfc From d9d25ac7be92f73b17bd175f65f35f10e158918d Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 1 Oct 2025 09:33:42 +0200 Subject: [PATCH 31/77] Fix some --- Mathlib/Tactic/DeclarationNames.lean | 2 +- Mathlib/Tactic/Linter/CommandStart.lean | 6 +++--- Mathlib/Tactic/Linter/Header.lean | 6 +++--- Mathlib/Tactic/ToAdditive/GuessName.lean | 4 ++-- Mathlib/Tactic/ToExpr.lean | 2 +- Mathlib/Tactic/Widget/Calc.lean | 4 ++-- Mathlib/Tactic/Widget/CongrM.lean | 3 ++- Mathlib/Tactic/Widget/Conv.lean | 3 ++- Mathlib/Tactic/Widget/GCongr.lean | 3 ++- Mathlib/Tactic/Widget/SelectPanelUtils.lean | 2 +- Mathlib/Util/Superscript.lean | 6 +++--- 11 files changed, 22 insertions(+), 19 deletions(-) diff --git a/Mathlib/Tactic/DeclarationNames.lean b/Mathlib/Tactic/DeclarationNames.lean index f16c295b8625c7..1a966d8c3b88e1 100644 --- a/Mathlib/Tactic/DeclarationNames.lean +++ b/Mathlib/Tactic/DeclarationNames.lean @@ -21,7 +21,7 @@ namespace Mathlib.Linter If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers for the names of the declarations whose syntax begins in position at least `pos`. -/ -def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos) : +def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) : m (Array Syntax) := do -- declarations from parallelism branches should not be interesting here, so use `local` let drs := declRangeExt.toPersistentEnvExtension.getState (asyncMode := .local) (← getEnv) diff --git a/Mathlib/Tactic/Linter/CommandStart.lean b/Mathlib/Tactic/Linter/CommandStart.lean index 50e29c0ca66d09..2da877818838af 100644 --- a/Mathlib/Tactic/Linter/CommandStart.lean +++ b/Mathlib/Tactic/Linter/CommandStart.lean @@ -50,7 +50,7 @@ formatting. This is every declaration until the type-specification, if there is one, or the value, as well as all `variable` commands. -/ -def CommandStart.endPos (stx : Syntax) : Option String.Pos := +def CommandStart.endPos (stx : Syntax) : Option String.Pos.Raw := if let some cmd := stx.find? (#[``Parser.Command.declaration, `lemma].contains ·.getKind) then if let some ind := cmd.find? (·.isOfKind ``Parser.Command.inductive) then match ind.find? (·.isOfKind ``Parser.Command.optDeclSig) with @@ -78,7 +78,7 @@ structure FormatError where /-- The distance to the end of the source string, as number of characters -/ srcNat : Nat /-- The distance to the end of the source string, as number of string positions -/ - srcEndPos : String.Pos + srcEndPos : String.Pos.Raw /-- The distance to the end of the formatted string, as number of characters -/ fmtPos : Nat /-- The kind of formatting error. For example: `extra space`, `remove line break` or @@ -90,7 +90,7 @@ structure FormatError where /-- The length of the mismatch, as number of characters. -/ length : Nat /-- The starting position of the mismatch, as a `String.pos`. -/ - srcStartPos : String.Pos + srcStartPos : String.Pos.Raw deriving Inhabited instance : ToString FormatError where diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index e2858ebd66c48e..83073d28e7d639 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -96,7 +96,7 @@ parsing the file linearly, it will only need to parse In conclusion, either the parsing is successful, and the linter can continue with its analysis, or the parsing is not successful and the linter will flag a missing module doc-string! -/ -def parseUpToHere (pos : String.Pos) (post : String := "") : CommandElabM Syntax := do +def parseUpToHere (pos : String.Pos.Raw) (post : String := "") : CommandElabM Syntax := do let upToHere : Substring := { str := (← getFileMap).source, startPos := ⟨0⟩, stopPos := pos } -- Append a further string after the content of `upToHere`. Parser.testParseModule (← getEnv) "linter.style.header" (upToHere.toString ++ post) @@ -104,7 +104,7 @@ def parseUpToHere (pos : String.Pos) (post : String := "") : CommandElabM Syntax /-- `toSyntax s pattern` converts the two input strings into a `Syntax`, assuming that `pattern` is a substring of `s`: the syntax is an atom with value `pattern` whose the range is the range of `pattern` in `s`. -/ -def toSyntax (s pattern : String) (offset : String.Pos := 0) : Syntax := +def toSyntax (s pattern : String) (offset : String.Pos.Raw := 0) : Syntax := let beg := ((s.splitOn pattern).getD 0 "").endPos + offset let fin := (((s.splitOn pattern).getD 0 "") ++ pattern).endPos + offset mkAtomFrom (.ofRange ⟨beg, fin⟩) pattern @@ -116,7 +116,7 @@ produces. `authorsLineChecks` computes a position for its warning *relative to `line`*. The `offset` input passes on the starting position of `line` in the whole file. -/ -def authorsLineChecks (line : String) (offset : String.Pos) : Array (Syntax × String) := +def authorsLineChecks (line : String) (offset : String.Pos.Raw) : Array (Syntax × String) := Id.run do -- We cannot reasonably validate the author names, so we look only for a few common mistakes: -- the line starting wrongly, double spaces, using ' and ' between names, diff --git a/Mathlib/Tactic/ToAdditive/GuessName.lean b/Mathlib/Tactic/ToAdditive/GuessName.lean index 0fdfa792d4ed0f..56413f743c9af1 100644 --- a/Mathlib/Tactic/ToAdditive/GuessName.lean +++ b/Mathlib/Tactic/ToAdditive/GuessName.lean @@ -35,7 +35,7 @@ open String in E.g. `#eval "InvHMulLEConjugate₂SMul_ne_top".splitCase` yields `["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]`. -/ -partial def _root_.String.splitCase (s : String) (i₀ : Pos := 0) (r : List String := []) : +partial def _root_.String.splitCase (s : String) (i₀ : Pos.Raw := 0) (r : List String := []) : List String := Id.run do -- We test if we need to split between `i₀` and `i₁`. let i₁ := s.next i₀ @@ -60,7 +60,7 @@ partial def _root_.String.splitCase (s : String) (i₀ : Pos := 0) (r : List Str return splitCase s i₁ r /-- Helper for `capitalizeLike`. -/ -partial def capitalizeLikeAux (s : String) (i : String.Pos := 0) (p : String) : String := +partial def capitalizeLikeAux (s : String) (i : String.Pos.Raw := 0) (p : String) : String := if p.atEnd i || s.atEnd i then p else diff --git a/Mathlib/Tactic/ToExpr.lean b/Mathlib/Tactic/ToExpr.lean index 72f4fd3b7ee873..5ed3ba1646dabd 100644 --- a/Mathlib/Tactic/ToExpr.lean +++ b/Mathlib/Tactic/ToExpr.lean @@ -21,7 +21,7 @@ instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where toExpr _ := mkConst ``PUnit.unit [toLevel.{u+1}] toTypeExpr := mkConst ``PUnit [toLevel.{u+1}] -deriving instance ToExpr for String.Pos +deriving instance ToExpr for String.Pos.Raw deriving instance ToExpr for Substring deriving instance ToExpr for SourceInfo deriving instance ToExpr for Syntax diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean index 68b1f92724c79a..c6f663b2a745b6 100644 --- a/Mathlib/Tactic/Widget/Calc.lean +++ b/Mathlib/Tactic/Widget/Calc.lean @@ -59,7 +59,7 @@ structure CalcParams extends SelectInsertParams where /-- Return the link text and inserted text above and below of the calc widget. -/ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (params : CalcParams) : - MetaM (String × String × Option (String.Pos × String.Pos)) := do + MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do let subexprPos := getGoalLocations pos let some (rel, lhs, rhs) ← Lean.Elab.Term.getCalcRelation? goalType | throwError "invalid 'calc' step, relation expected{indentExpr goalType}" @@ -108,7 +108,7 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par | true, true => "Create two new steps" | true, false | false, true => "Create a new step" | false, false => "This should not happen" - let pos : String.Pos := insertedCode.find (fun c => c == '?') + let pos : String.Pos.Raw := insertedCode.find (fun c => c == '?') return (stepInfo, insertedCode, some (pos, ⟨pos.byteIdx + 2⟩) ) /-- Rpc function for the calc widget. -/ diff --git a/Mathlib/Tactic/Widget/CongrM.lean b/Mathlib/Tactic/Widget/CongrM.lean index dcbd233639db96..a5650d414fb8f6 100644 --- a/Mathlib/Tactic/Widget/CongrM.lean +++ b/Mathlib/Tactic/Widget/CongrM.lean @@ -21,7 +21,8 @@ open Lean Meta Server ProofWidgets /-- Return the link text and inserted text above and below of the congrm widget. -/ @[nolint unusedArguments] def makeCongrMString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) - (_ : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do + (_ : SelectInsertParams) : + MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do let subexprPos := getGoalLocations pos unless goalType.isAppOf ``Eq || goalType.isAppOf ``Iff do throwError "The goal must be an equality or iff." diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean index d6331951af1e85..2684bb0d3f7894 100644 --- a/Mathlib/Tactic/Widget/Conv.lean +++ b/Mathlib/Tactic/Widget/Conv.lean @@ -86,7 +86,8 @@ open Lean Syntax in /-- Return the link text and inserted text above and below of the conv widget. -/ @[nolint unusedArguments] def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) - (params : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do + (params : SelectInsertParams) : + MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do let some pos := locations[0]? | throwError "You must select something." let (fvar, subexprPos) ← match pos with | ⟨_, .target subexprPos⟩ => pure (none, subexprPos) diff --git a/Mathlib/Tactic/Widget/GCongr.lean b/Mathlib/Tactic/Widget/GCongr.lean index c5d0b22d163a4a..0a198741f8f9ae 100644 --- a/Mathlib/Tactic/Widget/GCongr.lean +++ b/Mathlib/Tactic/Widget/GCongr.lean @@ -17,7 +17,8 @@ open Lean Meta Server ProofWidgets /-- Return the link text and inserted text above and below of the gcongr widget. -/ @[nolint unusedArguments] def makeGCongrString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) - (_ : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do + (_ : SelectInsertParams) : + MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do let subexprPos := getGoalLocations pos unless goalType.isAppOf ``LE.le || goalType.isAppOf ``LT.lt || goalType.isAppOf `Int.ModEq do panic! "The goal must be a ≤ or < or ≡." diff --git a/Mathlib/Tactic/Widget/SelectPanelUtils.lean b/Mathlib/Tactic/Widget/SelectPanelUtils.lean index 6ecdb2d975cf38..46733daefbecdf 100644 --- a/Mathlib/Tactic/Widget/SelectPanelUtils.lean +++ b/Mathlib/Tactic/Widget/SelectPanelUtils.lean @@ -74,7 +74,7 @@ We also make sure `mkCmdStr` is executed in the right context. -/ def mkSelectionPanelRPC {Params : Type} [SelectInsertParamsClass Params] (mkCmdStr : (pos : Array GoalsLocation) → (goalType : Expr) → Params → - MetaM (String × String × Option (String.Pos × String.Pos))) + MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))) (helpMsg : String) (title : String) (onlyGoal := true) (onlyOne := false) : (params : Params) → RequestM (RequestTask Html) := fun params ↦ RequestM.asTask do diff --git a/Mathlib/Util/Superscript.lean b/Mathlib/Util/Superscript.lean index f0a770f242e450..128c30a82e22ea 100644 --- a/Mathlib/Util/Superscript.lean +++ b/Mathlib/Util/Superscript.lean @@ -71,7 +71,7 @@ otherwise it will parse only 1. If successful, it passes the result to `k` as an where `a..b` is a token and `b..c` is whitespace. -/ partial def satisfyTokensFn (p : Char → Bool) (errorMsg : String) (many := true) - (k : Array (String.Pos × String.Pos × String.Pos) → ParserState → ParserState) : + (k : Array (String.Pos.Raw × String.Pos.Raw × String.Pos.Raw) → ParserState → ParserState) : ParserFn := fun c s => let start := s.pos let s := takeWhile1Fn p errorMsg c s @@ -124,7 +124,7 @@ partial def scriptFnNoAntiquot (m : Mapping) (errorMsg : String) (p : ParserFn) let mut newStr := "" -- This consists of a sorted array of `(from, to)` pairs, where indexes `from+i` in `newStr` -- such that `from+i < from'` for the next element of the array, are mapped to `to+i`. - let mut aligns := #[((0 : String.Pos), start)] + let mut aligns := #[((0 : String.Pos.Raw), start)] for (start, stopTk, stopWs) in toks do let mut pos := start while pos < stopTk do @@ -140,7 +140,7 @@ partial def scriptFnNoAntiquot (m : Mapping) (errorMsg : String) (p : ParserFn) let ictx := mkInputContext newStr "" let s' := p.run ictx c.toParserModuleContext c.tokens (mkParserState newStr) let rec /-- Applies the alignment mapping to a position. -/ - align (pos : String.Pos) := + align (pos : String.Pos.Raw) := let i := partitionPoint aligns (·.1 ≤ pos) let (a, b) := aligns[i - 1]! pos - a + b From 22a88b4aae03d5ae24afb0e5fabfe55f5265a56a Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 1 Oct 2025 10:40:13 +0200 Subject: [PATCH 32/77] Fix --- Mathlib/Data/String/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean index d70c1463bf3a03..221628123801fa 100644 --- a/Mathlib/Data/String/Basic.lean +++ b/Mathlib/Data/String/Basic.lean @@ -61,7 +61,7 @@ theorem ltb_cons_addChar' (c : Char) (s₁ s₂ : Iterator) : rw [ltb, Iterator.hasNext_cons_addChar, Iterator.hasNext_cons_addChar, if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih] · simp [Iterator.next, String.next, get_cons_addChar] - congr 2 <;> apply Pos.addChar_right_comm + congr 2 <;> apply Pos.Raw.addChar_right_comm · simpa [Iterator.curr, get_cons_addChar] using h | case2 s₁ s₂ h₁ h₂ h => rw [ltb, Iterator.hasNext_cons_addChar, Iterator.hasNext_cons_addChar, @@ -74,7 +74,7 @@ theorem ltb_cons_addChar' (c : Char) (s₁ s₂ : Iterator) : | case4 s₁ s₂ h₁ => rw [ltb, Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)] -theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos) : +theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos.Raw) : ltb ⟨mk (c :: cs₁), i₁ + c⟩ ⟨mk (c :: cs₂), i₂ + c⟩ = ltb ⟨mk cs₁, i₁⟩ ⟨mk cs₂, i₂⟩ := by rw [eq_comm, ← ltb_cons_addChar' c] simp @@ -96,13 +96,13 @@ theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList simp [Iterator.hasNext] · apply not_lt_of_gt; apply List.nil_lt_cons · rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb - simp only [Iterator.hasNext, Pos.byteIdx_zero, endPos_asString, utf8Len_cons, add_pos_iff, + simp only [Iterator.hasNext, Pos.Raw.byteIdx_zero, endPos_asString, utf8Len_cons, add_pos_iff, Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Iterator.curr, get, List.data_asString, utf8GetAux, Iterator.next, next, Bool.ite_eq_true_distrib, decide_eq_true_eq] simp only [← String.mk_eq_asString] split_ifs with h · subst c₂ - suffices ltb ⟨mk (c₁ :: cs₁), (0 : Pos) + c₁⟩ ⟨mk (c₁ :: cs₂), (0 : Pos) + c₁⟩ = + suffices ltb ⟨mk (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩ ⟨mk (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ = ltb ⟨mk cs₁, 0⟩ ⟨mk cs₂, 0⟩ by rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm apply ltb_cons_addChar · refine ⟨List.Lex.rel, fun e ↦ ?_⟩ From 0575c3e0def9b712e331557d045fd2cb5392199c Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 1 Oct 2025 09:02:52 +0000 Subject: [PATCH 33/77] chore: bump to nightly-2025-10-01 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1be8b1fbd7f8c6..9e81483fc72ce6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-09-30 +leanprover/lean4:nightly-2025-10-01 From 46eec1d7ebd24a7f8996b3ab416038c5cbffc02f Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Wed, 1 Oct 2025 10:59:46 +0000 Subject: [PATCH 34/77] chore: adaptations for nightly-2025-10-01 From 78792eb81ab910ff71bca01ee2d2516004f534be Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 1 Oct 2025 14:21:53 +0200 Subject: [PATCH 35/77] fix: remove unused simp arg due to changed definition of `OptionT.run_bind` --- Mathlib/Control/Monad/Cont.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Control/Monad/Cont.lean b/Mathlib/Control/Monad/Cont.lean index f7533c385485fa..304f443e0af161 100644 --- a/Mathlib/Control/Monad/Cont.lean +++ b/Mathlib/Control/Monad/Cont.lean @@ -8,7 +8,6 @@ import Mathlib.Control.Monad.Writer import Mathlib.Control.Lawful import Batteries.Tactic.Congr import Batteries.Lean.Except -import Batteries.Control.OptionT /-! # Continuation Monad @@ -179,8 +178,7 @@ instance [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m) where callCC_bind_left := by intros simp only [callCC, OptionT.callCC, OptionT.goto_mkLabel, bind_pure_comp, OptionT.run_bind, - OptionT.run_mk, Option.elimM_map, Option.elim_some, Function.comp_apply, - @callCC_bind_left m _] + OptionT.run_mk, Option.elimM_map, Option.elim_some, @callCC_bind_left m _] ext; rfl callCC_dummy := by intros; simp only [callCC, OptionT.callCC, @callCC_dummy m _]; ext; rfl From 47370e1454ac5e782f3429f7a89b2a947dfb3c58 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 2 Oct 2025 09:38:21 +0000 Subject: [PATCH 36/77] chore: bump to nightly-2025-10-02 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 9e81483fc72ce6..142d4698d3b4f0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-01 +leanprover/lean4:nightly-2025-10-02 From 472669a74f78b53aa2abf407435c6406d8d595d0 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 2 Oct 2025 12:46:33 +0200 Subject: [PATCH 37/77] lake update --- lake-manifest.json | 10 +++++----- lakefile.lean | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 046204a67d57e8..7664d2748ca6bb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407", + "rev": "84994683e0e9e455b98f9daade3bfc77643bf027", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.68", + "inputRev": "v0.0.75-pre3", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2e582a44b0150db152bff1c8484eb557fb5340da", + "rev": "ba88b081e2bea3981d4ff227d1e0d877661d7c76", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b8926eab9f5a2a9862011c698dcfdc175d5fb2c6", + "rev": "5462f4b0ac62917bea70eb2cdbf7b3a486d90828", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.lean b/lakefile.lean index 0035d75acfd377..72d5aadcfcfb71 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,9 +7,9 @@ open Lake DSL -/ require "leanprover-community" / "batteries" @ git "nightly-testing" -require "leanprover-community" / "Qq" @ git "master" +require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "nightly-testing" -require "leanprover-community" / "proofwidgets" @ git "v0.0.68" -- ProofWidgets should always be pinned to a specific version +require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre3" -- ProofWidgets should always be pinned to a specific version with NameMap.empty.insert `errorOnBuild "ProofWidgets not up-to-date. \ Please run `lake exe cache get` to fetch the latest ProofWidgets. \ From 7d12068e7f0e46989c41e93fcaf2400801750cfd Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 2 Oct 2025 14:21:58 +0200 Subject: [PATCH 38/77] We actually follow aesop master, not nightly-testing --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7664d2748ca6bb..a83e8046aa61c1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -45,10 +45,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fc97e592e3e150370f17a12e3613e96252c4d3d0", + "rev": "9e8de5716b162ec8983a89711a186d13ff871c22", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", diff --git a/lakefile.lean b/lakefile.lean index 72d5aadcfcfb71..3fae1e412e78d3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ open Lake DSL require "leanprover-community" / "batteries" @ git "nightly-testing" require "leanprover-community" / "Qq" @ git "nightly-testing" -require "leanprover-community" / "aesop" @ git "nightly-testing" +require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre3" -- ProofWidgets should always be pinned to a specific version with NameMap.empty.insert `errorOnBuild "ProofWidgets not up-to-date. \ From 605f3e0ef72f76ff80fd08482ccede97ebb3e342 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Thu, 2 Oct 2025 13:35:40 +0000 Subject: [PATCH 39/77] chore: adaptations for nightly-2025-10-02 From 238b3c751bd0c7990d1c7ac938f02f5cedbb3aa6 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 3 Oct 2025 07:44:41 +0200 Subject: [PATCH 40/77] Use docgen nightly-testing --- .github/workflows/nightly-docgen.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/nightly-docgen.yml b/.github/workflows/nightly-docgen.yml index d6dfc4f2e250ac..c2301ceb27fe90 100644 --- a/.github/workflows/nightly-docgen.yml +++ b/.github/workflows/nightly-docgen.yml @@ -57,7 +57,7 @@ jobs: [[require]] scope = "leanprover" name = "doc-gen4" - rev = "main" + rev = "nightly-testing" EOF # Initialise docbuild as a Lean project From 72f0b5eddc89fc2863c6bb548bd278b7796f8456 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Fri, 3 Oct 2025 17:26:55 +0000 Subject: [PATCH 41/77] chore: bump to nightly-2025-10-03 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 142d4698d3b4f0..f9322f23df2ae9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-02 +leanprover/lean4:nightly-2025-10-03 From 176ebb691065fa0386f9d41ae63f20e960389989 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sun, 5 Oct 2025 14:19:10 +0000 Subject: [PATCH 42/77] chore: bump to nightly-2025-10-05 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f9322f23df2ae9..1444e181e42233 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-03 +leanprover/lean4:nightly-2025-10-05 From 6683f5ddc87d7508320fa08ca604ab9769ea04df Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 5 Oct 2025 16:37:05 +0200 Subject: [PATCH 43/77] lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 960dfc9164129c..a9364a406d0560 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "408fad66ce900c4e47f7739ea4a68399f158297a", + "rev": "4583377d39b5120d713e65de4f632ea3a545fdeb", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From 8f7a78a3c364760dafa253e53992917d28d9183a Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 5 Oct 2025 16:43:22 +0200 Subject: [PATCH 44/77] lakefile babysitting: Qq -> nightly-testing --- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a9364a406d0560..c1b7816466580c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2e582a44b0150db152bff1c8484eb557fb5340da", + "rev": "ba88b081e2bea3981d4ff227d1e0d877661d7c76", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4583377d39b5120d713e65de4f632ea3a545fdeb", + "rev": "6d55a02d09b10da4222f7b81fd27f6e226449f89", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.lean b/lakefile.lean index b84590b90fb38d..3fae1e412e78d3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ open Lake DSL -/ require "leanprover-community" / "batteries" @ git "nightly-testing" -require "leanprover-community" / "Qq" @ git "master" +require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre3" -- ProofWidgets should always be pinned to a specific version with NameMap.empty.insert `errorOnBuild From ac8a764b52b88ac588443dbd5adc5c7a4dd5b623 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sun, 5 Oct 2025 18:36:23 +0000 Subject: [PATCH 45/77] Merge master into nightly-testing --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index c1b7816466580c..6eb7f343012cfc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d55a02d09b10da4222f7b81fd27f6e226449f89", + "rev": "a967ed96aaa0a37e408144e71b797f127b10cfa5", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From c870f76ad56ecde0826479ba3909949169264e42 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 6 Oct 2025 08:42:17 +0200 Subject: [PATCH 46/77] Fix --- .../SimplexCategory/GeneratorsRelations/NormalForms.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean index f02dcd2dddfb53..2891919b0bfd16 100644 --- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean +++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean @@ -263,7 +263,7 @@ lemma standardσ_simplicialInsert (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : simp only [standardσ_cons, Category.assoc, this, h_rec hL.tail (j + 1) (by grind) (by grind)] -attribute [local grind] simplicialInsert_length simplicialInsert_isAdmissible in +attribute [local grind! .] simplicialInsert_length simplicialInsert_isAdmissible in /-- Using `standardσ_simplicialInsert`, we can prove that every morphism satisfying `P_σ` is equal to some `standardσ` for some admissible list of indices. -/ theorem exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : P_σ f) : From 7d6d06d5006e3e86c11df71d2a298612d0b754ed Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 6 Oct 2025 09:54:26 +0200 Subject: [PATCH 47/77] Fix --- Mathlib/Tactic/ToExpr.lean | 3 +++ scripts/nolints.json | 3 ++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/Mathlib/Tactic/ToExpr.lean b/Mathlib/Tactic/ToExpr.lean index 5ed3ba1646dabd..a624008fcf9ffb 100644 --- a/Mathlib/Tactic/ToExpr.lean +++ b/Mathlib/Tactic/ToExpr.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kyle Miller -/ import Mathlib.Util.WhatsNew +import Mathlib.Tactic.AdaptationNote /-! # `ToExpr` instances for Mathlib @@ -12,6 +13,8 @@ import Mathlib.Util.WhatsNew namespace Mathlib open Lean +#adaptation_note /-- 2025-10-06 https://github.com/leanprover/lean4/issues/10678 + Added `docBlame` nolint for `Mathlib.instToExprULift_mathlib.toExpr` -/ set_option autoImplicit true in deriving instance ToExpr for ULift diff --git a/scripts/nolints.json b/scripts/nolints.json index 2d117b1ec9fa53..f340c574fc6e25 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -316,4 +316,5 @@ ["docBlame", "Mathlib.Meta.NormNum.evalLE.core.ratArm"], ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.intArm"], ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.nnratArm"], - ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.ratArm"]] + ["docBlame", "Mathlib.Meta.NormNum.evalLT.core.ratArm"], + ["docBlame", "Mathlib.instToExprULift_mathlib.toExpr"]] From 904d9aa32a55625ea137f6f7d952270e8a9e1a64 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 6 Oct 2025 11:00:05 +0200 Subject: [PATCH 48/77] Noshake --- scripts/noshake.json | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/noshake.json b/scripts/noshake.json index eb97867df63397..79a093ec1df471 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -225,6 +225,7 @@ ["ProofWidgets.Component.OfRpcMethod"], "Mathlib.Tactic.Widget.CommDiag": ["Mathlib.CategoryTheory.Category.Basic"], "Mathlib.Tactic.Use": ["Batteries.Logic", "Mathlib.Tactic.WithoutCDot"], + "Mathlib.Tactic.ToExpr": ["Mathlib.Tactic.AdaptationNote"], "Mathlib.Tactic.ToAdditive.Frontend": ["Lean.Meta.Tactic.TryThis"], "Mathlib.Tactic.TermCongr": ["Mathlib.Logic.Basic"], "Mathlib.Tactic.TautoSet": @@ -253,9 +254,9 @@ "Mathlib.Data.PNat.Defs"], "Mathlib.Tactic.Order.CollectFacts": ["Mathlib.Order.BoundedOrder.Basic", "Mathlib.Order.Lattice"], + "Mathlib.Tactic.NormNum.Parity": ["Mathlib.Algebra.Ring.Int.Parity"], "Mathlib.Tactic.NormNum.ModEq": ["Mathlib.Data.Int.ModEq", "Mathlib.Tactic.NormNum.DivMod"], - "Mathlib.Tactic.NormNum.Parity": ["Mathlib.Algebra.Ring.Int.Parity"], "Mathlib.Tactic.NormNum.Ineq": ["Mathlib.Algebra.Order.Field.Defs", "Mathlib.Algebra.Order.Monoid.WithTop"], "Mathlib.Tactic.NormNum.BigOperators": @@ -348,6 +349,7 @@ "Mathlib.Tactic.Algebraize": ["Mathlib.Algebra.Algebra.Tower"], "Mathlib.Std.Data.HashMap": ["Std.Data.HashMap.AdditionalOperations"], "Mathlib.RingTheory.SimpleModule.Basic": ["Mathlib.Data.Matrix.Mul"], + "Mathlib.RingTheory.PowerSeries.Restricted": ["Mathlib.Tactic.Bound"], "Mathlib.RingTheory.PowerSeries.Evaluation": ["Mathlib.RingTheory.PowerSeries.PiTopology"], "Mathlib.RingTheory.PowerSeries.Basic": @@ -362,7 +364,6 @@ ["Mathlib.LinearAlgebra.FreeModule.IdealQuotient"], "Mathlib.RingTheory.Finiteness.Defs": ["Mathlib.Data.Finsupp.Defs"], "Mathlib.RingTheory.Adjoin.Basic": ["Mathlib.LinearAlgebra.Finsupp.SumProd"], - "Mathlib.RingTheory.PowerSeries.Restricted": ["Mathlib.Tactic.Bound"], "Mathlib.RepresentationTheory.FdRep": ["Mathlib.CategoryTheory.Monoidal.Rigid.Braided"], "Mathlib.RepresentationTheory.FDRep": From 644eb460529e99de5bf3f1b68607574620b6c439 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Mon, 6 Oct 2025 09:23:28 +0000 Subject: [PATCH 49/77] chore: adaptations for nightly-2025-10-05 From 7bb1cf18dad0e818b2dacb14fe1625b7e45f85fe Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 6 Oct 2025 09:44:06 +0000 Subject: [PATCH 50/77] chore: bump to nightly-2025-10-06 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1444e181e42233..24b723cf52cb34 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-05 +leanprover/lean4:nightly-2025-10-06 From 446678c6ae84af896303a3a2462634cb7398d942 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Mon, 6 Oct 2025 11:44:35 +0000 Subject: [PATCH 51/77] chore: adaptations for nightly-2025-10-06 From 8d91f624110b1a319e25faa32bc52e52967880f3 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Mon, 6 Oct 2025 15:14:16 +0000 Subject: [PATCH 52/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/10606 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 6eb7f343012cfc..dda822f72f8c22 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a967ed96aaa0a37e408144e71b797f127b10cfa5", + "rev": "816b5dbd91421870471b7b6757a29d5caa84ff64", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-10606", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 3fae1e412e78d3..912edb51629d07 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-10606" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre3" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index 24b723cf52cb34..c40e09a66aaaed 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-06 +leanprover/lean4-pr-releases:pr-release-10606-7785875 From 4a3d124a4e36b0aa228201875addc2a741dbba13 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 6 Oct 2025 18:40:29 +0200 Subject: [PATCH 53/77] Fix CompileInductive --- Mathlib/Util/CompileInductive.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Util/CompileInductive.lean b/Mathlib/Util/CompileInductive.lean index 10b1c277551b19..b7ba69544cf1f2 100644 --- a/Mathlib/Util/CompileInductive.lean +++ b/Mathlib/Util/CompileInductive.lean @@ -176,7 +176,7 @@ def compileInductiveOnly (iv : InductiveVal) (rv : RecursorVal) (warn := true) : }] Compiler.CSimp.add name .global for name in iv.all do - for aux in [mkRecOnName name, mkBRecOnName name] do + for aux in [mkRecOnName name, (mkBRecOnName name).str "go", mkBRecOnName name] do if let some (.defnInfo dv) := (← getEnv).find? aux then compileDefn dv @@ -234,6 +234,7 @@ end Mathlib.Util -- `Nat.rec` already has a `@[csimp]` lemma in Lean. compile_def% Nat.recOn +compile_def% Nat.brecOn.go compile_def% Nat.brecOn compile_inductive% Prod compile_inductive% List From 873e009aedeb816734ce388ad830cac6ff9e68c1 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 7 Oct 2025 09:51:27 +0000 Subject: [PATCH 54/77] chore: bump to nightly-2025-10-07 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 24b723cf52cb34..aea1008f9337ef 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-06 +leanprover/lean4:nightly-2025-10-07 From ddad28b17c6993881da664af5a9ccd2671b4623a Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Tue, 7 Oct 2025 11:08:48 +0000 Subject: [PATCH 55/77] chore: adaptations for nightly-2025-10-07 From 66bf82f7f1f80884a306523d648d26fcdfd85747 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 7 Oct 2025 11:34:31 +0000 Subject: [PATCH 56/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/10606 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index dda822f72f8c22..7899f7521cae15 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "816b5dbd91421870471b7b6757a29d5caa84ff64", + "rev": "e3973b26a0d7d4e2f6668ad09bf2f09f351bc1f9", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10606", diff --git a/lean-toolchain b/lean-toolchain index c40e09a66aaaed..44f33761a1b787 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-10606-7785875 +leanprover/lean4-pr-releases:pr-release-10606-951cf64 From e70f51e9133fa095d2fe75761e556fdb0e1a21e8 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 8 Oct 2025 09:47:48 +0000 Subject: [PATCH 57/77] chore: bump to nightly-2025-10-08 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index aea1008f9337ef..a99ddefa99d39b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-07 +leanprover/lean4:nightly-2025-10-08 From c82874561d6d90db5248a5def2435a5f4af607f9 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 8 Oct 2025 12:18:44 +0000 Subject: [PATCH 58/77] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/10713 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 894d0a4cc60db0..7b9526d480ed85 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1660d4093339da30aa4f39815f7aad371719c2fb", + "rev": "e3e15d3f9b90bfd13b227d8de51c24315e580879", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-10713", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 3fae1e412e78d3..919452ced7e442 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-10713" require "leanprover-community" / "Qq" @ git "nightly-testing" require "leanprover-community" / "aesop" @ git "master" require "leanprover-community" / "proofwidgets" @ git "v0.0.75-pre3" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index aea1008f9337ef..8fe3ae136bc37d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-07 +leanprover/lean4-pr-releases:pr-release-10713-7889f54 From 771f466451fa7354e070f01240df71bc31dd65c7 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 8 Oct 2025 15:44:41 +0200 Subject: [PATCH 59/77] lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7b9526d480ed85..46020814f826d6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e3e15d3f9b90bfd13b227d8de51c24315e580879", + "rev": "58dcb47ca548996b134a9699af119514f184524b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10713", From 64aa11b32e44bea834d0e170e6d66fa2db0df7f8 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Wed, 8 Oct 2025 15:57:28 +0200 Subject: [PATCH 60/77] First batch --- Mathlib/Tactic/Linter/CommandStart.lean | 4 ++-- Mathlib/Tactic/Linter/DocString.lean | 2 +- Mathlib/Tactic/Linter/Header.lean | 4 ++-- Mathlib/Util/Superscript.lean | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Tactic/Linter/CommandStart.lean b/Mathlib/Tactic/Linter/CommandStart.lean index 2da877818838af..f4f1b58868b99f 100644 --- a/Mathlib/Tactic/Linter/CommandStart.lean +++ b/Mathlib/Tactic/Linter/CommandStart.lean @@ -332,8 +332,8 @@ def commandStartLinter : Linter where run := withSetOptionIn fun stx ↦ do let docStringEnd := docStringEnd.getTailPos? |>.getD default let forbidden := getUnlintedRanges unlintedNodes ∅ stx for s in scan do - let center := origSubstring.stopPos - s.srcEndPos - let rg : String.Range := ⟨center, center + s.srcEndPos - s.srcStartPos + ⟨1⟩⟩ + let center := origSubstring.stopPos.unoffsetBy s.srcEndPos + let rg : String.Range := ⟨center, center |>.offsetBy s.srcEndPos |>.unoffsetBy s.srcStartPos |>.increaseBy 1⟩ if s.msg.startsWith "Oh no" then Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg) m!"This should not have happened: please report this issue!" diff --git a/Mathlib/Tactic/Linter/DocString.lean b/Mathlib/Tactic/Linter/DocString.lean index e84e3fe3edcfa2..f41fb4f542cbcc 100644 --- a/Mathlib/Tactic/Linter/DocString.lean +++ b/Mathlib/Tactic/Linter/DocString.lean @@ -93,7 +93,7 @@ def docStringLinter : Linter where run := withSetOptionIn fun stx ↦ do let tail := docTrim.length -- `endRange` creates an 0-wide range `n` characters from the end of `docStx` let endRange (n : Nat) : Syntax := .ofRange - {start := docStx.getTailPos?.get! - ⟨n⟩, stop := docStx.getTailPos?.get! - ⟨n⟩} + {start := docStx.getTailPos?.get!.unoffsetBy ⟨n⟩, stop := docStx.getTailPos?.get!.unoffsetBy ⟨n⟩} if docTrim.takeRight 1 == "," then Linter.logLintIf linter.style.docString (endRange (docString.length - tail + 3)) s!"error: doc-strings should not end with a comma" diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index 83073d28e7d639..166f64f158db02 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -105,8 +105,8 @@ def parseUpToHere (pos : String.Pos.Raw) (post : String := "") : CommandElabM Sy is a substring of `s`: the syntax is an atom with value `pattern` whose the range is the range of `pattern` in `s`. -/ def toSyntax (s pattern : String) (offset : String.Pos.Raw := 0) : Syntax := - let beg := ((s.splitOn pattern).getD 0 "").endPos + offset - let fin := (((s.splitOn pattern).getD 0 "") ++ pattern).endPos + offset + let beg := ((s.splitOn pattern).getD 0 "").endPos.offsetBy offset + let fin := (((s.splitOn pattern).getD 0 "") ++ pattern).endPos.offsetBy offset mkAtomFrom (.ofRange ⟨beg, fin⟩) pattern /-- Return if `line` looks like a correct authors line in a copyright header. diff --git a/Mathlib/Util/Superscript.lean b/Mathlib/Util/Superscript.lean index 128c30a82e22ea..22d45dd037afce 100644 --- a/Mathlib/Util/Superscript.lean +++ b/Mathlib/Util/Superscript.lean @@ -143,7 +143,7 @@ partial def scriptFnNoAntiquot (m : Mapping) (errorMsg : String) (p : ParserFn) align (pos : String.Pos.Raw) := let i := partitionPoint aligns (·.1 ≤ pos) let (a, b) := aligns[i - 1]! - pos - a + b + pos.unoffsetBy a |>.offsetBy b let s := { s with pos := align s'.pos, errorMsg := s'.errorMsg } if s.hasError then return s let rec From ab0b3a78efa0c1e032fa55bb63d18cf91ba8c709 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 8 Oct 2025 16:02:12 +0200 Subject: [PATCH 61/77] Bump batteries --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0a1d2164e24c21..f46b65cbbb70c4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b038fd1e7c17510090454ba6bfcd38093c9acc62", + "rev": "3e3ab44725d62e3d15b0dbd1b261cf187a26b33b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From f444347e0d401b53c8ab8f503204bb42541985aa Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 8 Oct 2025 16:43:17 +0000 Subject: [PATCH 62/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/10713 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 46020814f826d6..e32b86910c231e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "58dcb47ca548996b134a9699af119514f184524b", + "rev": "6837767b9b398152d05e9bd6cdcdbd531febb64f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10713", diff --git a/lean-toolchain b/lean-toolchain index 8fe3ae136bc37d..4b386037f6a7f6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-10713-7889f54 +leanprover/lean4-pr-releases:pr-release-10713-3d5bb52 From 1714afe17e0817825f737a705eb591291c79da7d Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Thu, 9 Oct 2025 02:08:21 +0000 Subject: [PATCH 63/77] chore: adaptations for nightly-2025-10-08 From 0dbe1afc9dd610b74632b0d36a4272af6c898872 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 9 Oct 2025 07:30:36 +0200 Subject: [PATCH 64/77] Lake update --- lake-manifest.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e32b86910c231e..c0ff9ee31d39a3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9e8de5716b162ec8983a89711a186d13ff871c22", + "rev": "5cd4d7eb072d267662693c77c596db05c4079223", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6837767b9b398152d05e9bd6cdcdbd531febb64f", + "rev": "9cc409e680b7a816b06dd481831932948f40e0da", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10713", From d749e6deb4086364c7997651875404ad1fc6a0af Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 9 Oct 2025 07:06:25 +0000 Subject: [PATCH 65/77] Update lean-toolchain for https://github.com/leanprover/lean4/pull/10713 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c0ff9ee31d39a3..03dfa8bc66f3a4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9cc409e680b7a816b06dd481831932948f40e0da", + "rev": "ec39ab54ca71450490c2f82900bc7a7efc39a0ef", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10713", diff --git a/lean-toolchain b/lean-toolchain index 4b386037f6a7f6..a0626d8a21ca7b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-10713-3d5bb52 +leanprover/lean4-pr-releases:pr-release-10713-105377e From c1e2e72e6a759e7cd35595bcb01e1dadda64273f Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Thu, 9 Oct 2025 09:49:59 +0000 Subject: [PATCH 66/77] chore: bump to nightly-2025-10-09 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index a99ddefa99d39b..f87dc5556a9e0a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-08 +leanprover/lean4:nightly-2025-10-09 From 865a2e953eee00d3506967840f08c47d37333089 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Thu, 9 Oct 2025 11:04:32 +0000 Subject: [PATCH 67/77] chore: adaptations for nightly-2025-10-09 From d3b29f6bd668828711f3deb37b804439bb6f687b Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Fri, 10 Oct 2025 09:40:32 +0000 Subject: [PATCH 68/77] chore: bump to nightly-2025-10-10 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f87dc5556a9e0a..0707dd8947c026 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-09 +leanprover/lean4:nightly-2025-10-10 From df20867a9835bf94fef2af6864d129951f8da683 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 10 Oct 2025 12:55:41 +0200 Subject: [PATCH 69/77] lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 3199bbc7cd59fa..7a04fb75c0653e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dc646583b485257f603c261e359802dd61fa91f8", + "rev": "81fdb08a1272414aeaedec79a43d73050391fa32", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From dd2f0ecbb290a52325f4cbe4ef8a1ee669ab24d2 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 10 Oct 2025 14:01:22 +0200 Subject: [PATCH 70/77] lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7a04fb75c0653e..e1c7ee546264d6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "81fdb08a1272414aeaedec79a43d73050391fa32", + "rev": "0e17c69fe878d10d012867bfb122a91bfb85f9bd", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From ba09c433e308ab31159e3418e042940702bd349e Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 10 Oct 2025 14:03:07 +0200 Subject: [PATCH 71/77] lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index e1c7ee546264d6..26624e13b49de9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0e17c69fe878d10d012867bfb122a91bfb85f9bd", + "rev": "c82d1db7ac9aec6a06f39c3c18500bc5b36f13d7", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From e6b997b6f3745a60aba2c4bd810476889391c619 Mon Sep 17 00:00:00 2001 From: mathlib4-bot Date: Fri, 10 Oct 2025 14:00:55 +0000 Subject: [PATCH 72/77] chore: adaptations for nightly-2025-10-10 From a21c8bbb13ecd92dc0c838c4ffd2dc48a57390a8 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sat, 11 Oct 2025 09:36:32 +0000 Subject: [PATCH 73/77] chore: bump to nightly-2025-10-11 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 0707dd8947c026..ecaecb4ec60b1f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-10 +leanprover/lean4:nightly-2025-10-11 From 1e181d234aa5582f67b3a1771db9778b5e27c866 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sat, 11 Oct 2025 14:34:24 +0200 Subject: [PATCH 74/77] lake update --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 26624e13b49de9..bb775f941189bc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c82d1db7ac9aec6a06f39c3c18500bc5b36f13d7", + "rev": "8e55f5b88c9772b6adc1da0c6d4f6fccb29b5888", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From 9d611b790c52acf210d2e858dcfa9578aa3c50c8 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 12 Oct 2025 08:31:57 +0200 Subject: [PATCH 75/77] I shake it, I shake it, I shake it, ooh --- Mathlib/Data/Fin/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 0948db9876ea62..c6b2aac0de7b8c 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -6,7 +6,6 @@ Authors: Robert Y. Lewis, Keeley Hoek import Mathlib.Data.Int.DivMod import Mathlib.Order.Lattice import Mathlib.Tactic.Common -import Batteries.Data.Fin.Basic /-! # The finite type with `n` elements From f06bb3439ba08f5daf83e3953412c2f5b8fba018 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 12 Oct 2025 08:40:33 +0200 Subject: [PATCH 76/77] Noshake instead --- Mathlib/Data/Fin/Basic.lean | 1 + scripts/noshake.json | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index c6b2aac0de7b8c..0948db9876ea62 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -6,6 +6,7 @@ Authors: Robert Y. Lewis, Keeley Hoek import Mathlib.Data.Int.DivMod import Mathlib.Order.Lattice import Mathlib.Tactic.Common +import Batteries.Data.Fin.Basic /-! # The finite type with `n` elements diff --git a/scripts/noshake.json b/scripts/noshake.json index 2c16dd5553e768..2529928df56d93 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -49,8 +49,8 @@ "Mathlib.Data.Set.Notation", "Mathlib.Data.Sym.Sym2.Init", "Mathlib.Data.Vector.Basic", - "Mathlib.Geometry.Manifold.Notation", "Mathlib.Geometry.Manifold.Instances.Real", + "Mathlib.Geometry.Manifold.Notation", "Mathlib.Init", "Mathlib.LinearAlgebra.AffineSpace.Basic", "Mathlib.LinearAlgebra.Matrix.Notation", @@ -397,6 +397,7 @@ "Mathlib.Logic.Function.Defs": ["Mathlib.Tactic.AdaptationNote"], "Mathlib.Logic.Function.Basic": ["Batteries.Tactic.Init"], "Mathlib.Logic.Equiv.Prod": ["Mathlib.Data.Prod.PProd"], + "Mathlib.Logic.Equiv.Fin.Basic": ["Batteries.Data.Fin.Lemmas"], "Mathlib.Logic.Equiv.Defs": ["Mathlib.Data.Bool.Basic", "Mathlib.Data.Subtype"], "Mathlib.Logic.Basic": @@ -422,7 +423,8 @@ ["Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected", "Mathlib.Util.Superscript"], "Mathlib.Geometry.Manifold.Notation": - ["Mathlib.Geometry.Manifold.ContMDiff.Defs", "Mathlib.Geometry.Manifold.MFDeriv.Defs"], + ["Mathlib.Geometry.Manifold.ContMDiff.Defs", + "Mathlib.Geometry.Manifold.MFDeriv.Defs"], "Mathlib.Deprecated.NatLemmas": ["Batteries.Data.Nat.Lemmas", "Batteries.WF"], "Mathlib.Deprecated.MinMax": ["Mathlib.Order.MinMax"], "Mathlib.Deprecated.LazyList": ["Mathlib.Lean.Thunk"], From 2fd965ad0351ddcc7be19f0725df76a17df56e9f Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Sun, 12 Oct 2025 09:56:41 +0000 Subject: [PATCH 77/77] chore: bump to nightly-2025-10-12 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index ecaecb4ec60b1f..724c2b3ee8eb8c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-10-11 +leanprover/lean4:nightly-2025-10-12