From 315bc0d7d72734c560e70e85b975381dd61b8f64 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Mon, 1 Jun 2026 22:24:43 +0000 Subject: [PATCH 01/13] Update Batteries branch for testing https://github.com/leanprover-community/batteries/pull/1830 --- 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 59c01927aba2bb..028252c1d20751 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "708b057842c4cd0845fba132bd94b08493f6fc42", + "rev": "3f62d1e6130c646cfbd3e4d9fbe310e074044328", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc1", + "inputRev": "move-class-linter", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index b79c1398ff5cbc..77f9a67c758dc0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "v4.31.0-rc1" +require "leanprover-community" / "batteries" from git "https://github.com/leanprover-community/batteries" @ "move-class-linter" require "leanprover-community" / "Qq" @ git "v4.31.0-rc1" require "leanprover-community" / "aesop" @ git "v4.31.0-rc1" require "leanprover-community" / "proofwidgets" @ git "v0.0.100" From 3d77d522b3d845b9a9679fb649efaafcfcb46bb1 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Mon, 1 Jun 2026 22:49:02 +0000 Subject: [PATCH 02/13] Trigger CI for https://github.com/leanprover-community/batteries/pull/1830 --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 028252c1d20751..d5950da4b1017e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3f62d1e6130c646cfbd3e4d9fbe310e074044328", + "rev": "572905e6434111445fe81e4c3f4b42f197f24c9b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "move-class-linter", From a31d8c358fcc4b7d2416448c8b9ec39d4939771e Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 22 Jun 2026 10:04:24 -0400 Subject: [PATCH 03/13] fix --- Mathlib/SetTheory/Lists.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean index 970c56cfded6fc..e89fcda0ca58f5 100644 --- a/Mathlib/SetTheory/Lists.lean +++ b/Mathlib/SetTheory/Lists.lean @@ -9,7 +9,7 @@ public import Mathlib.Algebra.Order.Group.Nat public import Mathlib.Algebra.Order.Monoid.NatCast public import Mathlib.Algebra.Ring.Nat public import Mathlib.Data.Sigma.Basic -public import Batteries.Tactic.Lint.TypeClass +public import Batteries.Linter.TypeClass /-! # A computable model of ZFA without infinity From 2d9078e61eb02c7370684a01497b3c13ff962b6b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Mon, 22 Jun 2026 14:38:57 -0400 Subject: [PATCH 04/13] fix imports --- Mathlib/Tactic/Linter/Lint.lean | 1 + MathlibTest/BasicFiles/Init.lean | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 1b1bd995958ab8..2bb242c9aa7e36 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -9,6 +9,7 @@ module -- It is responsible for making `#lint` available through `Mathlib.Init`. -- TODO: consider removing `-- shake: keep` after batteries#1613 public import Batteries.Tactic.Lint -- shake: keep +public import Batteries.Linter -- shake: keep public import Lean.Linter.Deprecated public import Mathlib.Tactic.DeclarationNames public import Batteries.Tactic.Lint.Basic diff --git a/MathlibTest/BasicFiles/Init.lean b/MathlibTest/BasicFiles/Init.lean index 94acda24214958..4b620f666d39d5 100644 --- a/MathlibTest/BasicFiles/Init.lean +++ b/MathlibTest/BasicFiles/Init.lean @@ -1,6 +1,7 @@ module import Mathlib.Init +import Batteries.Linter.Frontend /-! Checks that some utilities are available already when importing `Mathlib.Init`. -/ @@ -33,7 +34,8 @@ import Mathlib.Init proof_wanted please_prove_this : True -- Guard against the shake tool modifying our imports -/-- info: [public import Init, public meta import Init, import Mathlib.Init] -/ +/-- info: [public import Init, public meta import Init, import Mathlib.Init, +import Batteries.Linter.Frontend] -/ #guard_msgs in run_elab Lean.logInfo m!"{(← Lean.MonadEnv.getEnv).imports}" From 31ed0e0266f1b47275bde7da1b80ad72ece70f77 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Mon, 22 Jun 2026 18:04:41 -0400 Subject: [PATCH 05/13] fix --- Mathlib/Algebra/Ring/Ext.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Ring/Ext.lean b/Mathlib/Algebra/Ring/Ext.lean index b024fdbee9ac42..1b76dbc2d48819 100644 --- a/Mathlib/Algebra/Ring/Ext.lean +++ b/Mathlib/Algebra/Ring/Ext.lean @@ -281,7 +281,7 @@ namespace Semiring inst₁ = inst₂ := by -- Show that enough substructures are equal. have h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid := by - ext : 1 <;> assumption + ext : 1; assumption have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by ext : 1 <;> assumption have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by @@ -290,7 +290,7 @@ namespace Semiring ext : 1; exact h_mul -- Split into fields and prove they are equal using the above. cases inst₁; cases inst₂ - congr <;> solve | injection h₁ | injection h₂ + congr; solve | injection h₁ | injection h₂ theorem toNonUnitalSemiring_injective : Function.Injective (@toNonUnitalSemiring R) := by From aa184a591c05ee81bbea1e06e98696839f32f9b2 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 22 Jun 2026 19:39:37 -0400 Subject: [PATCH 06/13] fix imports --- Mathlib/Algebra/Opposites.lean | 2 +- Mathlib/Data/List/Basic.lean | 2 +- Mathlib/Data/Option/Basic.lean | 2 +- Mathlib/Data/Seq/Computation.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Opposites.lean b/Mathlib/Algebra/Opposites.lean index b9d19e7f62af83..6fdb56716ab364 100644 --- a/Mathlib/Algebra/Opposites.lean +++ b/Mathlib/Algebra/Opposites.lean @@ -7,7 +7,7 @@ module public import Mathlib.Algebra.Group.Defs public import Mathlib.Logic.Equiv.Defs -public import Batteries.Tactic.Lint.Simp +public import Batteries.Linter.Simp /-! # Multiplicative opposite and algebraic operations on it diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 7934ab8744cd87..076714a9ed15b2 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -11,7 +11,7 @@ public import Mathlib.Logic.OpClass public import Mathlib.Logic.Unique public import Mathlib.Tactic.Common public import Batteries.Data.List.Lemmas -public import Batteries.Tactic.Lint.Simp +public import Batteries.Linter.Simp public import Batteries.Tactic.SeqFocus public import Mathlib.Data.Subtype public import Mathlib.Tactic.Attr.Core diff --git a/Mathlib/Data/Option/Basic.lean b/Mathlib/Data/Option/Basic.lean index e66b8f9b8b3ef2..b6f4f663e78ebe 100644 --- a/Mathlib/Data/Option/Basic.lean +++ b/Mathlib/Data/Option/Basic.lean @@ -11,7 +11,7 @@ public import Mathlib.Logic.IsEmpty.Basic public import Mathlib.Logic.Relator public import Mathlib.Util.CompileInductive public import Aesop -public import Batteries.Tactic.Lint.Simp +public import Batteries.Linter.Simp /-! # Option of a type diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean index 07b1fbbd784efd..57a6d36bf25a70 100644 --- a/Mathlib/Data/Seq/Computation.lean +++ b/Mathlib/Data/Seq/Computation.lean @@ -9,7 +9,7 @@ public import Mathlib.Data.Nat.Find public import Mathlib.Data.Stream.Init public import Mathlib.Logic.Relator public import Mathlib.Tactic.Common -public import Batteries.Tactic.Lint.Simp +public import Batteries.Linter.Simp /-! # Coinductive formalization of unbounded computations. From a5f51f6be27e1dcef170eb35fe07a353fea7edb1 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 23 Jun 2026 11:05:10 -0400 Subject: [PATCH 07/13] fix --- Mathlib/Tactic/CategoryTheory/Elementwise.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/CategoryTheory/Elementwise.lean b/Mathlib/Tactic/CategoryTheory/Elementwise.lean index 344e463d0a2a72..787cfc63c0e8f4 100644 --- a/Mathlib/Tactic/CategoryTheory/Elementwise.lean +++ b/Mathlib/Tactic/CategoryTheory/Elementwise.lean @@ -91,7 +91,7 @@ def elementwiseExpr (src : Name) (pf : Expr) (simpSides := true) : -- check that it's not a simp-trivial equality: forallTelescope ty' fun _ ty' => do if let some (_, lhs, rhs) := ty'.eq? then - if ← Batteries.Tactic.Lint.isSimpEq lhs rhs then + if ← Batteries.Linter.isSimpEq lhs rhs then throwError "applying simp to both sides reduces elementwise lemma for {src} \ to the trivial equality {ty'}. \ Either add `nosimp` or remove the `elementwise` attribute." From 28a05e5f02136458c4892f5c0a1a483dd61cdd72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Tue, 23 Jun 2026 17:15:53 -0400 Subject: [PATCH 08/13] fix --- Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean | 2 +- Mathlib/Lean/Elab/InfoTree.lean | 2 +- Mathlib/Tactic/Linter/UnusedInstancesInType.lean | 2 +- scripts/noshake.json | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean b/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean index 994a2c97d78546..b82d471bf69a82 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean @@ -6,7 +6,7 @@ Authors: Kim Morrison, Johannes Hölzl, Reid Barton, Sean Leather module public import Mathlib.Init -public import Batteries.Tactic.Lint.Misc +public import Batteries.Linter.Misc /-! # Bundled types diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean index cca33050a3b0e2..8add19c3fd8945 100644 --- a/Mathlib/Lean/Elab/InfoTree.lean +++ b/Mathlib/Lean/Elab/InfoTree.lean @@ -8,7 +8,7 @@ module public import Mathlib.Lean.Environment public import Lean.Server.InfoUtils public import Lean.Meta.TryThis -public import Batteries.Tactic.Lint.Misc +public import Batteries.Linter.Misc -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. import Mathlib.Tactic.Linter.Header -- shake: keep diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean index 4a6ec648aff168..d09e3c8da81270 100644 --- a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean +++ b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean @@ -13,7 +13,7 @@ public meta import Lean.Linter.Basic -- this file has a valid copyright header and module docstring. public import Mathlib.Tactic.Linter.Header -- shake: keep public import Batteries.Tactic.Lint.Basic -public import Batteries.Tactic.Lint.Misc +public import Batteries.Linter.Misc /-! # Linters for Unused Instances in Types diff --git a/scripts/noshake.json b/scripts/noshake.json index b2d50ab4febb68..b25ec069dc3490 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -14,7 +14,7 @@ "Batteries.Tactic.HaveI", "Batteries.Tactic.LeftRight", "Batteries.Tactic.Lint", - "Batteries.Tactic.Lint.Misc", + "Batteries.Linter.Misc", "Batteries.Tactic.NoMatch", "Batteries.Tactic.NormCast", "Batteries.Tactic.NormCast.Lemmas", From 9677580b2d1145d244fac37296bcc679da14bdae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Tue, 23 Jun 2026 18:19:26 -0400 Subject: [PATCH 09/13] fix: directory dependency --- Mathlib/Tactic/Linter/DirectoryDependency.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index 4fae86eecdf634..84e5290ea22871 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -183,6 +183,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Util.FormatTable, `Mathlib.Data.String.Defs), (`Mathlib.Lean, `Batteries.Tactic.Lint), + (`Mathlib.Lean, `Batteries.Linter), (`Mathlib.Lean, `Batteries.CodeAction), -- TODO: should this be minimised further? (`Mathlib.Lean.Meta.CongrTheorems, `Batteries), From de9aa46e0de5d1d3a58acb699f673f95d5e86210 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 23 Jun 2026 20:45:21 -0400 Subject: [PATCH 10/13] fix --- Mathlib/Data/List/Defs.lean | 2 +- Mathlib/Lean/Elab/InfoTree.lean | 2 +- Mathlib/Tactic/Linarith/Lemmas.lean | 2 +- Mathlib/Tactic/Linter/Lint.lean | 4 ++-- Mathlib/Tactic/Linter/Style.lean | 2 +- Mathlib/Tactic/Linter/TacticDocumentation.lean | 2 +- Mathlib/Tactic/Linter/UnusedInstancesInType.lean | 2 +- 7 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean index d77363c4f50ddc..a12e2e0110fd11 100644 --- a/Mathlib/Data/List/Defs.lean +++ b/Mathlib/Data/List/Defs.lean @@ -9,7 +9,7 @@ public import Mathlib.Data.Nat.Notation public import Mathlib.Control.Functor public import Mathlib.Data.SProd public import Mathlib.Util.CompileInductive -public import Batteries.Tactic.Lint.Basic +public import Batteries.Linter.Basic public import Batteries.Data.List.Basic public import Batteries.Logic diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean index 8add19c3fd8945..51677f36b27c13 100644 --- a/Mathlib/Lean/Elab/InfoTree.lean +++ b/Mathlib/Lean/Elab/InfoTree.lean @@ -12,7 +12,7 @@ public import Batteries.Linter.Misc -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. import Mathlib.Tactic.Linter.Header -- shake: keep -public import Batteries.Tactic.Lint.Basic +public import Batteries.Linter.Basic import Lean.Elab.Term.TermElabM /-! diff --git a/Mathlib/Tactic/Linarith/Lemmas.lean b/Mathlib/Tactic/Linarith/Lemmas.lean index c44b8b9b4d45d3..cd0f7897013b4d 100644 --- a/Mathlib/Tactic/Linarith/Lemmas.lean +++ b/Mathlib/Tactic/Linarith/Lemmas.lean @@ -5,7 +5,7 @@ Authors: Robert Y. Lewis -/ module -public meta import Batteries.Tactic.Lint.Basic +public meta import Batteries.Linter.Basic public meta import Mathlib.Data.Ineq public import Mathlib.Data.Ineq public import Mathlib.Data.Nat.Cast.Order.Ring diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 2bb242c9aa7e36..afe93af1504473 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -5,14 +5,14 @@ Authors: Floris van Doorn -/ module --- This module imports all of `Batteries.Tactic.Lint`, not just `Batteries.Tactic.Lint.Basic`. +-- This module imports all of `Batteries.Tactic.Lint`, not just `Batteries.Linter.Basic`. -- It is responsible for making `#lint` available through `Mathlib.Init`. -- TODO: consider removing `-- shake: keep` after batteries#1613 public import Batteries.Tactic.Lint -- shake: keep public import Batteries.Linter -- shake: keep public import Lean.Linter.Deprecated public import Mathlib.Tactic.DeclarationNames -public import Batteries.Tactic.Lint.Basic +public import Batteries.Linter.Basic /-! # Linters for Mathlib diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean index d949f89d541593..dc148d87395fab 100644 --- a/Mathlib/Tactic/Linter/Style.lean +++ b/Mathlib/Tactic/Linter/Style.lean @@ -12,7 +12,7 @@ public meta import Lean.Server.InfoUtils public meta import Mathlib.Tactic.Linter.Header -- shake: keep public import Lean.Parser.Command public import Mathlib.Tactic.DeclarationNames -public import Batteries.Tactic.Lint.Basic +public import Batteries.Linter.Basic /-! ## Style linters diff --git a/Mathlib/Tactic/Linter/TacticDocumentation.lean b/Mathlib/Tactic/Linter/TacticDocumentation.lean index bd0874afb9d480..7da6fcd7e2bc8a 100644 --- a/Mathlib/Tactic/Linter/TacticDocumentation.lean +++ b/Mathlib/Tactic/Linter/TacticDocumentation.lean @@ -10,7 +10,7 @@ public meta import Lean.Parser.Tactic.Doc -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public import Mathlib.Tactic.Linter.Header -- shake: keep -public import Batteries.Tactic.Lint.Basic +public import Batteries.Linter.Basic public import Lean.Elab.Tactic.Doc /-! # The `tacticDocs` linter diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean index d09e3c8da81270..c7bf5d91c76784 100644 --- a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean +++ b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean @@ -12,7 +12,7 @@ public meta import Lean.Linter.Basic -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public import Mathlib.Tactic.Linter.Header -- shake: keep -public import Batteries.Tactic.Lint.Basic +public import Batteries.Linter.Basic public import Batteries.Linter.Misc /-! From 17bbd0075c32c793bc988b8d36ab49a8c79b6678 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 23 Jun 2026 21:15:24 -0400 Subject: [PATCH 11/13] fix --- Mathlib/Tactic/Linter/Style.lean | 4 ++-- Mathlib/Tactic/Linter/TacticDocumentation.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean index dc148d87395fab..3f4d2729220c5a 100644 --- a/Mathlib/Tactic/Linter/Style.lean +++ b/Mathlib/Tactic/Linter/Style.lean @@ -551,10 +551,10 @@ public def isBadNameWithUnderscore (name : Name) : Bool := Id.run do if declName.toString.contains "_" then return true else return false -open Batteries.Tactic.Lint in +open Batteries.Linter in /-- Linter that checks for definitions whose name contains an underscore: such names violate the naming convention. -/ -@[env_linter] public def defsWithUnderscore : Batteries.Tactic.Lint.Linter where +@[env_linter] public def defsWithUnderscore : Batteries.Linter where noErrorsFound := "no definitions with an underscore in their name found." errorsFound := "FOUND definitions with an underscore in their name." test declName := do diff --git a/Mathlib/Tactic/Linter/TacticDocumentation.lean b/Mathlib/Tactic/Linter/TacticDocumentation.lean index 7da6fcd7e2bc8a..47bb3ec20858a7 100644 --- a/Mathlib/Tactic/Linter/TacticDocumentation.lean +++ b/Mathlib/Tactic/Linter/TacticDocumentation.lean @@ -28,7 +28,7 @@ meta def isNonemptyDoc (doc : TacticDoc) : Bool := doc.docString.isSome || doc.extensionDocs.any (! ·.isEmpty) /-- Check that all tactics available in Mathlib have a docstring. -/ -@[env_linter] public meta def tacticDocs : Batteries.Tactic.Lint.Linter where +@[env_linter] public meta def tacticDocs : Batteries.Linter where noErrorsFound := "No tactics are missing documentation." errorsFound := "TACTICS ARE MISSING DOCUMENTATION STRINGS:" test tac := do From b36f42a3f7c30c33b1cefeb2f377b07ebb3864d7 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Wed, 24 Jun 2026 13:21:57 -0400 Subject: [PATCH 12/13] fix --- Mathlib/Tactic/Linter/Lint.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index afe93af1504473..1c3f0771841e38 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -5,10 +5,9 @@ Authors: Floris van Doorn -/ module --- This module imports all of `Batteries.Tactic.Lint`, not just `Batteries.Linter.Basic`. +-- This module imports all of `Batteries.Linter`, not just `Batteries.Linter.Basic`. -- It is responsible for making `#lint` available through `Mathlib.Init`. -- TODO: consider removing `-- shake: keep` after batteries#1613 -public import Batteries.Tactic.Lint -- shake: keep public import Batteries.Linter -- shake: keep public import Lean.Linter.Deprecated public import Mathlib.Tactic.DeclarationNames From 933cc59231e8e5d259c61cab8f740b0e36169d5a Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Wed, 24 Jun 2026 13:37:29 -0400 Subject: [PATCH 13/13] fix --- Mathlib/Init.lean | 2 +- Mathlib/Tactic/Linter/DirectoryDependency.lean | 1 - Mathlib/Tactic/Linter/Lint.lean | 4 ++-- scripts/noshake.json | 2 +- 4 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index e49829ccc5766f..895c4d49541cf3 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -35,7 +35,7 @@ public import Batteries.Util.ProofWanted -- This import makes the `#redundant_imports`/`#min_imports`/`#find_home`/`#import_diff` commands -- available globally. public import ImportGraph.Tools --- The following module imports `Batteries.Tactic.Lint`, where `#lint` is defined. +-- The following module imports `Batteries.Linter`, where `#lint` is defined. public import Mathlib.Tactic.Linter.Lint -- This import makes the `#min_imports in` command available globally. public import Mathlib.Tactic.MinImports diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index 84e5290ea22871..0110d5bb76f5a5 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -182,7 +182,6 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ -- TODO: reduce this dependency by upstreaming `Data.String.Defs to batteries (`Mathlib.Util.FormatTable, `Mathlib.Data.String.Defs), - (`Mathlib.Lean, `Batteries.Tactic.Lint), (`Mathlib.Lean, `Batteries.Linter), (`Mathlib.Lean, `Batteries.CodeAction), -- TODO: should this be minimised further? diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean index 1c3f0771841e38..2ac8670edfff11 100644 --- a/Mathlib/Tactic/Linter/Lint.lean +++ b/Mathlib/Tactic/Linter/Lint.lean @@ -24,7 +24,7 @@ Perhaps these should be moved to Batteries in the future. meta section -namespace Batteries.Tactic.Lint +namespace Batteries.Linter open Lean Meta /-- @@ -56,7 +56,7 @@ Linter that checks whether a structure should be in Prop. | some _ => return none -- TODO: enforce `YYYY-MM-DD` format | none => return m!"`deprecated` attribute without `since` date" -end Batteries.Tactic.Lint +end Batteries.Linter namespace Mathlib.Linter diff --git a/scripts/noshake.json b/scripts/noshake.json index b25ec069dc3490..80bec325ccffc7 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -13,7 +13,7 @@ "Batteries.Tactic.GuardMsgs", "Batteries.Tactic.HaveI", "Batteries.Tactic.LeftRight", - "Batteries.Tactic.Lint", + "Batteries.Linter", "Batteries.Linter.Misc", "Batteries.Tactic.NoMatch", "Batteries.Tactic.NormCast",