chore: adaptations for batteries#1830

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

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

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

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

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
 

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

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.

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

Mathlib/Lean/Elab/InfoTree.lean

@@ -8,11 +8,11 @@ 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
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 import Lean.Elab.Term.TermElabM
 
 /-!

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

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."

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

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -182,7 +182,7 @@ 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?
   (`Mathlib.Lean.Meta.CongrTheorems, `Batteries),

Mathlib/Tactic/Linter/Lint.lean

@@ -5,13 +5,13 @@ 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.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
-public import Batteries.Tactic.Lint.Basic
+public import Batteries.Linter.Basic
 
 /-!
 # Linters for Mathlib
@@ -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
 

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
@@ -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

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
@@ -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

Mathlib/Tactic/Linter/UnusedInstancesInType.lean

@@ -12,8 +12,8 @@ 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.Tactic.Lint.Misc
+public import Batteries.Linter.Basic
+public import Batteries.Linter.Misc
 
 /-!
 # Linters for Unused Instances in Types

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}"
 

lake-manifest.json

@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f",
+   "rev": "c35ff55997866abfddeb272c3a293f941fb37f65",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "move-class-linter",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.lean

@@ -6,10 +6,10 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "main"
-require "leanprover-community" / "Qq" @ git "master"
-require "leanprover-community" / "aesop" @ git "master"
-require "leanprover-community" / "proofwidgets" @ git "main"
+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"
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets failed to reuse pre-built JS code. \
     Please report this issue on the Lean Zulip."

scripts/noshake.json

@@ -13,8 +13,8 @@
   "Batteries.Tactic.GuardMsgs",
   "Batteries.Tactic.HaveI",
   "Batteries.Tactic.LeftRight",
-  "Batteries.Tactic.Lint",
-  "Batteries.Tactic.Lint.Misc",
+  "Batteries.Linter",
+  "Batteries.Linter.Misc",
   "Batteries.Tactic.NoMatch",
   "Batteries.Tactic.NormCast",
   "Batteries.Tactic.NormCast.Lemmas",