diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean index 6faace7d9609d0..fed2951bafd707 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean @@ -7,8 +7,8 @@ module public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex public import Mathlib.Algebra.Homology.HomotopyCategory.Shift -public import Mathlib.CategoryTheory.Shift.ShiftedHom public import Mathlib.Algebra.Module.Equiv.Basic +public import Mathlib.CategoryTheory.Shift.ShiftedHom public import Mathlib.Tactic.Linarith /-! # Shifting cochains diff --git a/Mathlib/Algebra/Lie/Solvable.lean b/Mathlib/Algebra/Lie/Solvable.lean index 52702b3c575477..62a6d5f736bf29 100644 --- a/Mathlib/Algebra/Lie/Solvable.lean +++ b/Mathlib/Algebra/Lie/Solvable.lean @@ -6,8 +6,8 @@ Authors: Oliver Nash module public import Mathlib.Algebra.Lie.BaseChange -public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic public import Mathlib.Algebra.Lie.Quotient +public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic /-! # Solvable Lie algebras diff --git a/Mathlib/Analysis/LocallyConvex/Asymptotics.lean b/Mathlib/Analysis/LocallyConvex/Asymptotics.lean index b391ac749d3807..0dd65e8900bf32 100644 --- a/Mathlib/Analysis/LocallyConvex/Asymptotics.lean +++ b/Mathlib/Analysis/LocallyConvex/Asymptotics.lean @@ -5,8 +5,8 @@ Authors: Anatole Dedecker, Moritz Doll -/ module -public import Mathlib.Analysis.Asymptotics.TVS public import Mathlib.Analysis.Asymptotics.Basic +public import Mathlib.Analysis.Asymptotics.TVS public import Mathlib.Analysis.LocallyConvex.WithSeminorms /-! diff --git a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean index 206e093b50b027..9b0550bfb15a3d 100644 --- a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean +++ b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean @@ -5,8 +5,8 @@ Authors: Jireh Loreaux -/ module -public import Mathlib.Analysis.Normed.Algebra.GelfandRadius public import Mathlib.Analysis.Calculus.Deriv.Basic +public import Mathlib.Analysis.Normed.Algebra.GelfandRadius public import Mathlib.Analysis.Normed.Algebra.Spectrum public import Mathlib.Analysis.Normed.Operator.Mul diff --git a/Mathlib/Basic/Logic/Basic.lean b/Mathlib/Basic/Logic/Basic.lean index 672430cad17ed0..873da0354e2fb0 100644 --- a/Mathlib/Basic/Logic/Basic.lean +++ b/Mathlib/Basic/Logic/Basic.lean @@ -5,10 +5,10 @@ Authors: Jeremy Avigad, Leonardo de Moura -/ module -public import Batteries.Logic -public import Batteries.Util.LibraryNote public meta import Mathlib.Lean.Meta.Simp public meta import Mathlib.Tactic.Attr.Register +public import Batteries.Logic +public import Batteries.Util.LibraryNote /-! # Basic logic properties diff --git a/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean b/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean index 14eea2b87a6c31..4586d8b4478799 100644 --- a/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean +++ b/Mathlib/CategoryTheory/Functor/Derived/RightDerivedCompositionCommShift.lean @@ -5,8 +5,8 @@ Authors: Joël Riou -/ module -public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift +public import Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition /-! # Compatibility with shifts of the comparison morphism for the composition of right derived functors diff --git a/Mathlib/CategoryTheory/Linear/Yoneda.lean b/Mathlib/CategoryTheory/Linear/Yoneda.lean index a8324e48202675..7cfe55cc8c1e37 100644 --- a/Mathlib/CategoryTheory/Linear/Yoneda.lean +++ b/Mathlib/CategoryTheory/Linear/Yoneda.lean @@ -5,8 +5,8 @@ Authors: Kim Morrison -/ module -public import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic public import Mathlib.CategoryTheory.Linear.LinearFunctor +public import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic /-! # The Yoneda embedding for `R`-linear categories diff --git a/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean b/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean index deca0151b66100..6939f23c4b4516 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean @@ -10,7 +10,6 @@ public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite import Mathlib.Combinatorics.Pigeonhole import Mathlib.Combinatorics.SimpleGraph.Bipartite - import Mathlib.Tactic.LinearCombination /-! diff --git a/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean b/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean index fde053db96e12d..1de60de2fdd0d5 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/ContinuousAlternatingMap.lean @@ -5,10 +5,10 @@ Authors: Sébastien Gouëzel -/ module +public import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.VectorBundle.Hom -public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable -public import Mathlib.Geometry.Manifold.Notation +public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap /-! # The bundle of alternating maps between `C^n` vector bundles over the same base space is `C^n` diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index 068997e6b342c8..597a4b7b3ae705 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -1,11 +1,7 @@ module -- shake: keep-all, shake: keep-downstream --- This import makes the `alias` command available globally. -public import Batteries.Tactic.Alias -- This import makes the `#help` command available globally. public meta import Batteries.Tactic.HelpCmd --- This import makes the `proof_wanted` command available globally. -public import Batteries.Util.ProofWanted -- This import makes the `#redundant_imports`/`#min_imports`/`#find_home`/`#import_diff` commands -- available globally. public meta import ImportGraph.Tools @@ -43,6 +39,10 @@ public meta import Mathlib.Tactic.TacticAnalysis.Declarations public meta import Mathlib.Tactic.TypeStar -- This import makes the binder plicity code action available globally public meta import Mathlib.Util.CodeActions +-- This import makes the `alias` command available globally. +public import Batteries.Tactic.Alias +-- This import makes the `proof_wanted` command available globally. +public import Batteries.Util.ProofWanted /-! This is the root file in Mathlib: it is imported by virtually *all* Mathlib files. diff --git a/Mathlib/Lean/CoreM.lean b/Mathlib/Lean/CoreM.lean index a64a7da261cfe8..5676cf38e7c50d 100644 --- a/Mathlib/Lean/CoreM.lean +++ b/Mathlib/Lean/CoreM.lean @@ -5,8 +5,8 @@ Authors: Kim Morrison -/ module -public import Mathlib.Init public import Lean.CoreM +public import Mathlib.Init /-! # Additional functions using `CoreM` state. diff --git a/Mathlib/Lean/Json.lean b/Mathlib/Lean/Json.lean index 378592fb19d195..ab703755b70b86 100644 --- a/Mathlib/Lean/Json.lean +++ b/Mathlib/Lean/Json.lean @@ -5,8 +5,8 @@ Authors: Eric Wieser -/ module -public import Mathlib.Init public import Lean.Data.Json.FromToJson.Basic +public import Mathlib.Init /-! # Json serialization typeclass for `PUnit` & `Fin n` & `Subtype p` diff --git a/Mathlib/Lean/Meta/CongrTheorems.lean b/Mathlib/Lean/Meta/CongrTheorems.lean index 4a8c7889db5928..23580de0cef924 100644 --- a/Mathlib/Lean/Meta/CongrTheorems.lean +++ b/Mathlib/Lean/Meta/CongrTheorems.lean @@ -5,9 +5,9 @@ Authors: Kyle Miller -/ module +public meta import Lean.Meta.CongrTheorems public meta import Lean.Meta.Tactic.Refl public meta import Mathlib.Basic.IsEmpty.Defs -public meta import Lean.Meta.CongrTheorems public import Mathlib.Basic.IsEmpty.Defs /-! diff --git a/Mathlib/Lean/Meta/DiscrTree.lean b/Mathlib/Lean/Meta/DiscrTree.lean index 257081b6d7a0f1..3359a3ca796523 100644 --- a/Mathlib/Lean/Meta/DiscrTree.lean +++ b/Mathlib/Lean/Meta/DiscrTree.lean @@ -5,10 +5,10 @@ Authors: Kim Morrison -/ module -public import Mathlib.Init public import Lean.Meta.Basic public import Lean.Meta.DiscrTree.Main public import Lean.Meta.DiscrTree.Types +public import Mathlib.Init /-! # Additions to `Lean.Meta.DiscrTree` diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean index 8007904d8b9179..a8e722d831385a 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean @@ -5,8 +5,8 @@ Authors: Jovan Gerbscheid -/ module -public import Mathlib.Init public import Lean.Meta.Basic +public import Mathlib.Init /-! # Basic Definitions for `RefinedDiscrTree` diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean index f88533d8c44fd0..166f5eb0220049 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean @@ -5,10 +5,10 @@ Authors: Jovan Gerbscheid -/ module +public import Lean.Linter.Deprecated public import Mathlib.Lean.Meta.RefinedDiscrTree.Basic import Lean.Meta.CompletionName -public import Lean.Linter.Deprecated /-! # Constructing a RefinedDiscrTree diff --git a/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean b/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean index ba72f6464a459a..c45f5d0dbf123b 100644 --- a/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean +++ b/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean @@ -10,9 +10,9 @@ public import Mathlib.LinearAlgebra.PiTensorProduct.Basic public import Mathlib.LinearAlgebra.TensorProduct.Map import Mathlib.Data.Set.Card +import Mathlib.LinearAlgebra.Finsupp.LinearCombination import Mathlib.LinearAlgebra.Quotient.Basic import Mathlib.SetTheory.Cardinal.Finite -import Mathlib.LinearAlgebra.Finsupp.LinearCombination /-! # Generators of multiple tensor products diff --git a/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean b/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean index f3d223704f5753..464ed6c62c50d7 100644 --- a/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/TotalVariation/Basic.lean @@ -5,9 +5,9 @@ Authors: Rémy Degenne -/ module +public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs -public import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym diff --git a/Mathlib/NumberTheory/NumberField/AdeleRing.lean b/Mathlib/NumberTheory/NumberField/AdeleRing.lean index ff287057a4d2be..1ec4ff0ba53a8f 100644 --- a/Mathlib/NumberTheory/NumberField/AdeleRing.lean +++ b/Mathlib/NumberTheory/NumberField/AdeleRing.lean @@ -5,8 +5,8 @@ Authors: Salvatore Mercuri, María Inés de Frutos-Fernández -/ module -public import Mathlib.NumberTheory.NumberField.InfiniteAdeleRing public import Mathlib.NumberTheory.NumberField.FiniteAdeleRing +public import Mathlib.NumberTheory.NumberField.InfiniteAdeleRing /-! # The adele ring of a number field diff --git a/Mathlib/Order/Notation.lean b/Mathlib/Order/Notation.lean index 813292397a956b..ff58e9afe6128b 100644 --- a/Mathlib/Order/Notation.lean +++ b/Mathlib/Order/Notation.lean @@ -7,9 +7,9 @@ module public meta import Lean.PrettyPrinter.Delaborator.Builtins public meta import Mathlib.Lean.PrettyPrinter.Delaborator +public meta import Qq public import Mathlib.Tactic.Simps public import Mathlib.Tactic.ToDual -public meta import Qq /-! # Notation classes for lattice operations diff --git a/Mathlib/Tactic/AdaptationNote.lean b/Mathlib/Tactic/AdaptationNote.lean index 71cfa35f1aaad8..ce914c2a33f486 100644 --- a/Mathlib/Tactic/AdaptationNote.lean +++ b/Mathlib/Tactic/AdaptationNote.lean @@ -6,10 +6,10 @@ Authors: Kyle Miller module public meta import Lean.Meta.Tactic.TryThis +public meta import Lean.Meta.TryThis -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Meta.TryThis /-! # Adaptation notes diff --git a/Mathlib/Tactic/Bound/Attribute.lean b/Mathlib/Tactic/Bound/Attribute.lean index c23f44494301e8..63cc475ec120f2 100644 --- a/Mathlib/Tactic/Bound/Attribute.lean +++ b/Mathlib/Tactic/Bound/Attribute.lean @@ -6,8 +6,8 @@ Authors: Geoffrey Irving module public meta import Aesop -public import Mathlib.Tactic.Bound.Init public meta import Qq +public import Mathlib.Tactic.Bound.Init /-! # The `bound` attribute diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean index 1a8cf863352e33..1d19614636e42e 100644 --- a/Mathlib/Tactic/CategoryTheory/Coherence.lean +++ b/Mathlib/Tactic/CategoryTheory/Coherence.lean @@ -6,8 +6,8 @@ Authors: Kim Morrison, Yuma Mizuno, Oleksandr Manzyuk module public meta import Lean.Meta.Tactic.Congr -public import Mathlib.CategoryTheory.Monoidal.Free.Basic public meta import Mathlib.Lean.Meta +public import Mathlib.CategoryTheory.Monoidal.Free.Basic public import Mathlib.Tactic.CategoryTheory.BicategoryCoherence public import Mathlib.Tactic.CategoryTheory.MonoidalComp diff --git a/Mathlib/Tactic/ClickSuggestions.lean b/Mathlib/Tactic/ClickSuggestions.lean index 072557f0efb351..4bc1d97e9e35e3 100644 --- a/Mathlib/Tactic/ClickSuggestions.lean +++ b/Mathlib/Tactic/ClickSuggestions.lean @@ -6,9 +6,9 @@ Authors: Jovan Gerbscheid module public meta import Lean.Server.FileWorker.RequestHandling +public meta import Lean.Widget.InteractiveGoal public meta import Mathlib.Lean.GoalsLocation public meta import Mathlib.Lean.Meta.KAbstractPositions -public meta import Lean.Widget.InteractiveGoal public import Mathlib.Tactic.ClickSuggestions.TryPremises public import Mathlib.Tactic.ClickSuggestions.Unfold public import ProofWidgets.Component.OfRpcMethod diff --git a/Mathlib/Tactic/ClickSuggestions/SectionState.lean b/Mathlib/Tactic/ClickSuggestions/SectionState.lean index b5c0eac219b0ae..710ab270988c3c 100644 --- a/Mathlib/Tactic/ClickSuggestions/SectionState.lean +++ b/Mathlib/Tactic/ClickSuggestions/SectionState.lean @@ -5,9 +5,9 @@ Authors: Jovan Gerbscheid -/ module +public meta import ProofWidgets.Component.FilterDetails public meta import ProofWidgets.Util public import Mathlib.Tactic.ClickSuggestions.Util -public meta import ProofWidgets.Component.FilterDetails /-! # Infrastructure for searching and displaying sets of lemmas diff --git a/Mathlib/Tactic/ClickSuggestions/Util.lean b/Mathlib/Tactic/ClickSuggestions/Util.lean index e692aa7ea91d36..2501a35cb2a417 100644 --- a/Mathlib/Tactic/ClickSuggestions/Util.lean +++ b/Mathlib/Tactic/ClickSuggestions/Util.lean @@ -6,15 +6,15 @@ Authors: Jovan Gerbscheid module public meta import Lean.PrettyPrinter.Delaborator.Builtins +public meta import Lean.Server.Utils public meta import Mathlib.Data.String.Defs +public meta import ProofWidgets.Component.MakeEditLink +public meta import ProofWidgets.Component.RefreshComponent public import Batteries.Tactic.PermuteGoals -public meta import Lean.Server.Utils public import Mathlib.Tactic.DepRewrite public import Mathlib.Tactic.GRewrite public import Mathlib.Tactic.NthRewrite public import Mathlib.Tactic.SimpRw -public meta import ProofWidgets.Component.MakeEditLink -public meta import ProofWidgets.Component.RefreshComponent /-! # Various utilities used in `#click_suggestions` diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index 22a50145f78688..57d01c6e1c08b4 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -124,6 +124,9 @@ public import Mathlib.Util.WhatsNew public meta import Lean.Elab.Tactic.Try public meta import Lean.Meta.Tactic.Try.Collect +-- Preserve custom import ordering: +set_option linter.style.header.imports false + /-! # Common tactics, linters, and utilities diff --git a/Mathlib/Tactic/DeclarationNames.lean b/Mathlib/Tactic/DeclarationNames.lean index 03a508f99f5b3f..bd71ca21e32903 100644 --- a/Mathlib/Tactic/DeclarationNames.lean +++ b/Mathlib/Tactic/DeclarationNames.lean @@ -6,11 +6,11 @@ Authors: Damiano Testa, Moritz Firsching module public meta import Lean.DeclarationRange +public meta import Lean.Message public meta import Lean.ResolveName -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! This file contains functions that are used by multiple linters. diff --git a/Mathlib/Tactic/DepRewrite.lean b/Mathlib/Tactic/DepRewrite.lean index 881b0560442d1b..d59439642e94b5 100644 --- a/Mathlib/Tactic/DepRewrite.lean +++ b/Mathlib/Tactic/DepRewrite.lean @@ -5,11 +5,11 @@ Authors: Aaron Liu, Wojciech Nawrocki -/ module +public meta import Lean.Elab.ConfigEval public meta import Lean.Elab.ConfigEval.Basic public meta import Lean.Elab.Tactic.Conv.Basic public meta import Lean.Elab.Tactic.Rewrite public meta import Lean.Elab.Tactic.Simp -public meta import Lean.Elab.ConfigEval meta import Lean.Elab.ConfigEval.DeriveEvalExpr meta import Lean.Elab.ConfigEval.DeriveEvalTerm diff --git a/Mathlib/Tactic/Eval.lean b/Mathlib/Tactic/Eval.lean index 062afd26c1ba90..1a22bf8fce90fa 100644 --- a/Mathlib/Tactic/Eval.lean +++ b/Mathlib/Tactic/Eval.lean @@ -5,8 +5,8 @@ Authors: Eric Wieser -/ module -public import Mathlib.Init public meta import Qq.Macro +public import Mathlib.Init /-! # The `eval%` term elaborator diff --git a/Mathlib/Tactic/FunProp/Core.lean b/Mathlib/Tactic/FunProp/Core.lean index 8604dd4cbe62f8..ac69d279b8e3be 100644 --- a/Mathlib/Tactic/FunProp/Core.lean +++ b/Mathlib/Tactic/FunProp/Core.lean @@ -9,9 +9,9 @@ public meta import Mathlib.Lean.Expr.Basic public meta import Mathlib.Tactic.FunProp.Theorems public meta import Mathlib.Tactic.FunProp.ToBatteries public meta import Mathlib.Tactic.FunProp.Types +public meta import Qq public import Batteries.Tactic.Exact public import Mathlib.Tactic.FunProp.Theorems -public meta import Qq /-! # Tactic `fun_prop` for proving function properties like `Continuous f`, `Differentiable ℝ f`, ... diff --git a/Mathlib/Tactic/FunProp/Types.lean b/Mathlib/Tactic/FunProp/Types.lean index ab4c755362bbda..032fe1ef9a5838 100644 --- a/Mathlib/Tactic/FunProp/Types.lean +++ b/Mathlib/Tactic/FunProp/Types.lean @@ -5,9 +5,9 @@ Authors: Tomáš Skřivan -/ module +public meta import Lean.Meta.Tactic.Simp public meta import Mathlib.Lean.Meta.RefinedDiscrTree.Basic public meta import Mathlib.Tactic.FunProp.FunctionData -public meta import Lean.Meta.Tactic.Simp /-! ## `funProp` diff --git a/Mathlib/Tactic/GrindAttrs.lean b/Mathlib/Tactic/GrindAttrs.lean index 21e0124caa133b..44d47e61d0c656 100644 --- a/Mathlib/Tactic/GrindAttrs.lean +++ b/Mathlib/Tactic/GrindAttrs.lean @@ -7,9 +7,9 @@ Authors: Floris van Doorn module public import Lean.Meta.Tactic.Grind.RegisterCommand +public import Std.Data.HashSet.Basic import Mathlib.Init -public import Std.Data.HashSet.Basic /-! # Custom grind-sets diff --git a/Mathlib/Tactic/Linter/AuxLemma.lean b/Mathlib/Tactic/Linter/AuxLemma.lean index ac1728bd645dd7..07626f64d3c33b 100644 --- a/Mathlib/Tactic/Linter/AuxLemma.lean +++ b/Mathlib/Tactic/Linter/AuxLemma.lean @@ -6,10 +6,10 @@ Authors: Kim Morrison module public meta import Lean.Elab.Command +public meta import Lean.Message -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! # The `auxLemma` linter diff --git a/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean b/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean index 475d172bc1adc8..fcc921163974f1 100644 --- a/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean +++ b/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa, Jeremy Tan, Adomas Baliuka module public meta import Lean.Elab.Command +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # Linter against deprecated syntax diff --git a/Mathlib/Tactic/Linter/DocPrime.lean b/Mathlib/Tactic/Linter/DocPrime.lean index 0e2c30e6111949..4712681ac2d123 100644 --- a/Mathlib/Tactic/Linter/DocPrime.lean +++ b/Mathlib/Tactic/Linter/DocPrime.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module public meta import Lean.Elab.Command +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # The "docPrime" linter diff --git a/Mathlib/Tactic/Linter/DocString.lean b/Mathlib/Tactic/Linter/DocString.lean index 151b457db2772e..114f7141f8b864 100644 --- a/Mathlib/Tactic/Linter/DocString.lean +++ b/Mathlib/Tactic/Linter/DocString.lean @@ -5,12 +5,12 @@ Authors: Michael Rothgang, Damiano Testa -/ module +public meta import Lean.DocString.Parser +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep public meta import Std.Data.Iterators.Combinators.Zip -public meta import Lean.DocString.Parser -public meta import Lean.Parser.Command meta import Std.Data.Iterators.Producers.Range diff --git a/Mathlib/Tactic/Linter/EmptyLine.lean b/Mathlib/Tactic/Linter/EmptyLine.lean index 5b87f7645d65f5..9ac5bdc0dcfdad 100644 --- a/Mathlib/Tactic/Linter/EmptyLine.lean +++ b/Mathlib/Tactic/Linter/EmptyLine.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # The "emptyLine" linter diff --git a/Mathlib/Tactic/Linter/FlexibleLinter.lean b/Mathlib/Tactic/Linter/FlexibleLinter.lean index dc034cb71da2b0..c58712a3355a73 100644 --- a/Mathlib/Tactic/Linter/FlexibleLinter.lean +++ b/Mathlib/Tactic/Linter/FlexibleLinter.lean @@ -9,10 +9,10 @@ public meta import Lean.Elab.Command public meta import Lean.Elab.InfoTree.Util public meta import Lean.Elab.Tactic.Simp public meta import Lean.Meta.Tactic.TryThis +public meta import Lean.Parser.Term -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Term /-! # The "flexible" linter diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index 1252410425e7bb..4a47d7be892b58 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module public meta import Lean.Elab.Command +public meta import Lean.Parser.Command -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Command /-! # `#`-command linter diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean index d3ebda59e52b0f..4371a6182f4432 100644 --- a/Mathlib/Tactic/Linter/Header.lean +++ b/Mathlib/Tactic/Linter/Header.lean @@ -5,11 +5,11 @@ Authors: Michael Rothgang, Damiano Testa, Thomas R. Murrills -/ module -public meta import Lean.Elab.Command +public meta import ImportGraph.Imports.Pretty +public meta import Lean.Linter.Basic public meta import Std.Sync.Mutex public meta import Lean.Parser.Module public import Mathlib.Tactic.Linter.DirectoryDependency -public meta import Lean.Linter.Basic public import Std.Sync.Mutex /-! @@ -47,7 +47,7 @@ a module doc-string (unless the command is exempted for some reason). meta section -open Lean Elab Command Linter +open ImportGraph Lean Elab Command Linter namespace Mathlib.Linter @@ -233,34 +233,16 @@ public register_option linter.style.header.license : String := { descr := "The text required as the second line of the copyright header." } -/-- Extends `Import` with ``stx : TSyntax `Lean.Parser.Module.import`` to allow reporting at the -given import. -/ -structure ImportRef extends Import where - stx : TSyntax ``Parser.Module.import - -/-- Returns the module `Ident` (following `(public)? (meta)? import (all)?` of a given -`ImportRef`. -/ -def ImportRef.getIdent (i : ImportRef) : Ident := - match i.stx with - | `(Parser.Module.import| - $[public]? $[meta]? import $[all]? $n:ident) => n - | _ => ⟨.missing⟩ - -/-- Destructures header syntax (`(module)? (prelude)? $imports*`) into an array of `ImportRef`s. -/ -def headerToImportRefs (header : TSyntax ``Parser.Module.header) : Array ImportRef := - match header with - | `(Parser.Module.header| $[module%$moduleTk]? $[prelude]? $imports*) => - imports.filterMap fun - | stx@`(Parser.Module.import| - $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n:ident) => - some { - module := n.getId - importAll := allTk.isSome - isExported := publicTk.isSome || moduleTk.isNone - isMeta := metaTk.isSome - stx := ⟨stx⟩ } - | _ => none - | _ => #[] +/-- +Whether to reformat import blocks in the module system according to the style convention. Note that +this only has an effect if `linter.style.header` is `true` and the header is participating in the +module system. This does not remove redundant imports. +-/ +public register_option linter.style.header.imports : Bool := { + defValue := true + descr := "Whether to reformat module system import blocks according to the style convention when \ + `linter.style.header` is `true`." +} /-- Returns the `module` token from header syntax, if there is one. -/ def headerToModuleTk? (header : TSyntax ``Parser.Module.header) : Option Syntax := @@ -283,6 +265,8 @@ because they are files that test the linter. def headerTestFiles : NameSet := .ofList [ `MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, + `MathlibTest.Linter.Header.ImportFormat, + `MathlibTest.Linter.Header.ImportFormatOff, `MathlibTest.Linter.Header.Verso, `MathlibTest.DirectoryDependencyLinter.Test] @@ -334,6 +318,32 @@ def duplicateImportsCheck (imports : Array ImportRef) : CommandElabM Unit := do else importsSoFar := importsSoFar.insert imp.toImport +/-- +If we are in the module system and `linter.style.header.imports` is `true`, reformat imports. + +Note that this assumes the check for `linter.style.header` has already been performed. +-/ +def formatImports (imports : Array (ImportRef × Import.Whitespace)) : CommandElabM Unit := do + unless + (← getEnv).header.isModule && getLinterValue linter.style.header.imports (← getLinterOptions) + do + return + let some (lastImportRef, _) := imports.back? | return + let impsRef := mkNullNode <| imports.map (·.1.stx) + let some (msg, errs) ← liftCoreM <| + Import.mkImportSuggestionMessage impsRef (imports.map (·.1.toImport)) imports + | return + let note := .note m!"This linter can be disabled by writing \ + `set_option {linter.style.header.imports.name} false` just after the import block." + if errs.isEmpty then + -- Note: when `errs.isEmpty`, `Import.mkImportSuggestionMessage` gives us a clickable widget + -- that uses `diffGranularity := .word`. This effectively gives us a newline before `{msg}`, + -- meaning we don't need one after `reformatted:` here. + logWarningAt lastImportRef.stx m!"Imports can be reformatted:{msg}{note}" + else + logWarningAt lastImportRef.stx m!"Imports can be reformatted, but some comments could not be \ + carried over. Please review the comment that will be inserted after the imports.\n{msg}{note}" + section HeaderParser open Lean.ParseImports @@ -376,6 +386,9 @@ partial def allowedHeaderParser : Parser := keyword "doc.verso.module", -- check last, otherwise it prevents hitting the ones it is a prefix of keyword "doc.verso", + keyword "linter.style.header.license", + keyword "linter.style.header.imports", + -- check last, otherwise it prevents hitting the ones it is a prefix of keyword "linter.style.header" -- for testing and downstream ] >> boolLit) @@ -424,7 +437,11 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do -- Re-parse the header slowly, to get the leading whitespace and nice source locations for imports let (headerStx, s, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName)) if log.hasErrors then return - let importRefs := headerToImportRefs headerStx + let importRefsWithWhitespace := headerToImportRefsWithWhitespace headerStx + -- TODO: Enable this more broadly (Archive, etc., and downstream) + if mainModule.getRoot == `Mathlib || headerTestFiles.contains mainModule then + formatImports importRefsWithWhitespace + let importRefs := importRefsWithWhitespace.map (·.1) -- Report on broad or duplicate imports. broadImportsCheck importRefs mainModule duplicateImportsCheck importRefs diff --git a/Mathlib/Tactic/Linter/InternalConstructor.lean b/Mathlib/Tactic/Linter/InternalConstructor.lean index 37a73315a2efcc..f26d9e53e182f2 100644 --- a/Mathlib/Tactic/Linter/InternalConstructor.lean +++ b/Mathlib/Tactic/Linter/InternalConstructor.lean @@ -7,10 +7,10 @@ module public meta import Lean.Elab.InfoTree.Util public meta import Lean.Linter.Basic +public meta import Lean.Message -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! # Linting against internal constructors diff --git a/Mathlib/Tactic/Linter/Multigoal.lean b/Mathlib/Tactic/Linter/Multigoal.lean index 55abfd7d84f995..71833faf100a08 100644 --- a/Mathlib/Tactic/Linter/Multigoal.lean +++ b/Mathlib/Tactic/Linter/Multigoal.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module public meta import Lean.Elab.Command +public meta import Lean.Parser.Term -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Parser.Term /-! # The "multiGoal" linter diff --git a/Mathlib/Tactic/Linter/OldObtain.lean b/Mathlib/Tactic/Linter/OldObtain.lean index c13f1a8b012aa0..0718424902565f 100644 --- a/Mathlib/Tactic/Linter/OldObtain.lean +++ b/Mathlib/Tactic/Linter/OldObtain.lean @@ -6,10 +6,10 @@ Authors: Michael Rothgang module public meta import Lean.Elab.Command +public meta import Lean.Message -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Message /-! # The `oldObtain` linter, against stream-of-consciousness `obtain` diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean index 36630d3f15eb10..d1cce77d20044b 100644 --- a/Mathlib/Tactic/Linter/Style.lean +++ b/Mathlib/Tactic/Linter/Style.lean @@ -5,13 +5,13 @@ Authors: Michael Rothgang -/ module +public meta import Batteries.Tactic.Lint.Basic +public meta import Batteries.Util.ExtendedBinder public meta import Lean.Elab.Command +public meta import Lean.Parser.Module -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Batteries.Tactic.Lint.Basic -public meta import Batteries.Util.ExtendedBinder -public meta import Lean.Parser.Module public import Mathlib.Tactic.DeclarationNames meta import Lean.Parser.Command diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean index 4c4babb8887807..e3837eae63d586 100644 --- a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean +++ b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean @@ -6,12 +6,12 @@ Authors: Thomas R. Murrills module public meta import Batteries.Lean.Position +public meta import Batteries.Tactic.Lint.Basic +public meta import Batteries.Tactic.Lint.Misc public meta import Lean.Linter.Basic public meta import Mathlib.Lean.Elab.InfoTree public meta import Mathlib.Lean.Environment public meta import Mathlib.Lean.Expr.Basic -public meta import Batteries.Tactic.Lint.Basic -public meta import Batteries.Tactic.Lint.Misc -- 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 diff --git a/Mathlib/Tactic/Linter/UnusedTactic.lean b/Mathlib/Tactic/Linter/UnusedTactic.lean index 18484768aa78a4..2907a244036857 100644 --- a/Mathlib/Tactic/Linter/UnusedTactic.lean +++ b/Mathlib/Tactic/Linter/UnusedTactic.lean @@ -6,11 +6,11 @@ Authors: Damiano Testa module public meta import Lean.Elab.InfoTree.Util +public meta import Lean.Parser.Syntax -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep public import Batteries.Tactic.Unreachable -public meta import Lean.Parser.Syntax public import Mathlib.Tactic.Linter.UnusedTacticExtension /-! diff --git a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean index 806f763ec54e90..728809ffb2fa67 100644 --- a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean +++ b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean @@ -6,10 +6,10 @@ Authors: Damiano Testa module +public meta import Lean.Exception -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Exception /-! This file defines the environment extension to keep track of which tactics are allowed to leave diff --git a/Mathlib/Tactic/Matrix/MulExpand.lean b/Mathlib/Tactic/Matrix/MulExpand.lean index c0f7fd6453654a..03e7216b79dd74 100644 --- a/Mathlib/Tactic/Matrix/MulExpand.lean +++ b/Mathlib/Tactic/Matrix/MulExpand.lean @@ -7,9 +7,9 @@ module public meta import Mathlib.Tactic.Matrix.ListMatrix public meta import Mathlib.Util.Qq +public meta import Qq public import Batteries.Logic -- shake: keep (Qq dependency) public import Mathlib.Init -public meta import Qq /-! # Expansion of products of list matrices diff --git a/Mathlib/Tactic/MinImports.lean b/Mathlib/Tactic/MinImports.lean index a150d26813dd00..cf4d6471aab893 100644 --- a/Mathlib/Tactic/MinImports.lean +++ b/Mathlib/Tactic/MinImports.lean @@ -7,12 +7,12 @@ module public meta import ImportGraph.Imports.Redundant public meta import ImportGraph.Imports.RequiredModules +public meta import Lean.Elab.DeclModifiers public meta import Lean.Elab.DefView public meta import Lean.Util.CollectAxioms -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. public meta import Mathlib.Tactic.Linter.Header -- shake: keep -public meta import Lean.Elab.DeclModifiers /-! # `#min_imports in` a command to find minimal imports diff --git a/Mathlib/Tactic/Nontriviality/Core.lean b/Mathlib/Tactic/Nontriviality/Core.lean index 1b7177ed4aa9cb..12474b89c419e9 100644 --- a/Mathlib/Tactic/Nontriviality/Core.lean +++ b/Mathlib/Tactic/Nontriviality/Core.lean @@ -7,11 +7,11 @@ module public meta import Lean.Elab.Tactic.Meta public meta import Lean.Elab.Tactic.SolveByElim +public meta import Qq.Macro public meta import Qq.MetaM +public meta import Qq.Typ public import Mathlib.Basic.Nontrivial.Basic -- shake: keep (tactic dependency) public import Mathlib.Tactic.Attr.Register -- shake: keep (tactic dependency) -public meta import Qq.Macro -public meta import Qq.Typ /-! # The `nontriviality` tactic. -/ diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean index ad1c541ee293ef..68abff57947d0b 100644 --- a/Mathlib/Tactic/NormNum/Core.lean +++ b/Mathlib/Tactic/NormNum/Core.lean @@ -5,10 +5,10 @@ Authors: Mario Carneiro -/ module +public meta import Lean.Elab.Tactic.Try -- shake: keep (`register_try?_tactic` command dependency) public meta import Lean.Meta.Tactic.Try.Collect public meta import Mathlib.Lean.Expr.Rat public meta import Mathlib.Util.Qq -public meta import Lean.Elab.Tactic.Try -- shake: keep (`register_try?_tactic` command dependency) public import Mathlib.Tactic.NormNum.Result /-! diff --git a/Mathlib/Tactic/NormNum/NatLog.lean b/Mathlib/Tactic/NormNum/NatLog.lean index e6a0163bc4e5ad..417faf980b1e3f 100644 --- a/Mathlib/Tactic/NormNum/NatLog.lean +++ b/Mathlib/Tactic/NormNum/NatLog.lean @@ -5,8 +5,8 @@ Authors: Kyle Miller, Andreas Gittis -/ module -public meta import Mathlib.Data.Nat.Log public meta import Batteries.Lean.Expr +public meta import Mathlib.Data.Nat.Log public import Mathlib.Data.Nat.Log public import Mathlib.Tactic.NormNum diff --git a/Mathlib/Tactic/NormNum/Pow.lean b/Mathlib/Tactic/NormNum/Pow.lean index c8b8d28b70111f..c2ea38afea1ed3 100644 --- a/Mathlib/Tactic/NormNum/Pow.lean +++ b/Mathlib/Tactic/NormNum/Pow.lean @@ -5,9 +5,9 @@ Authors: Mario Carneiro, Thomas Murrills -/ module +public meta import Mathlib.Util.Qq public import Mathlib.Data.Int.Cast.Lemmas public import Mathlib.Tactic.NormNum.Basic -public meta import Mathlib.Util.Qq /-! ## `norm_num` plugin for `^`. diff --git a/Mathlib/Tactic/SetLike.lean b/Mathlib/Tactic/SetLike.lean index 1d51f675ff329a..1c6436ac5f5bb1 100644 --- a/Mathlib/Tactic/SetLike.lean +++ b/Mathlib/Tactic/SetLike.lean @@ -5,9 +5,9 @@ Authors: Jireh Loreaux -/ module -public meta import Batteries.Util.LibraryNote public meta import Aesop.Frontend public meta import Aesop.Frontend.Basic +public meta import Batteries.Util.LibraryNote public import Batteries.Util.LibraryNote import Mathlib.Init diff --git a/Mathlib/Tactic/TacticAnalysis.lean b/Mathlib/Tactic/TacticAnalysis.lean index 56550c5ed03368..cc666b0e9a0815 100644 --- a/Mathlib/Tactic/TacticAnalysis.lean +++ b/Mathlib/Tactic/TacticAnalysis.lean @@ -6,10 +6,10 @@ Authors: Anne Baanen module public meta import Lean.Compiler.IR.CompilerM +public meta import Lean.Elab.Command public meta import Lean.Elab.InfoTree.Util public meta import Lean.Util.Heartbeats public meta import Mathlib.Lean.Elab.Tactic.Meta -public meta import Lean.Elab.Command public import Mathlib.Lean.ContextInfo /-! # Tactic analysis framework diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean index d7d1c9fb58754c..ac9c7511497f4e 100644 --- a/Mathlib/Tactic/Tauto.lean +++ b/Mathlib/Tactic/Tauto.lean @@ -8,10 +8,10 @@ module public meta import Lean.Elab.ConfigEval public meta import Lean.Elab.Tactic.Classical public meta import Mathlib.Lean.Meta +public meta import Qq public import Mathlib.Basic.Logic.Basic -- shake: keep (dependency of tactic output) public import Mathlib.Tactic.CasesM public import Mathlib.Tactic.Core -public meta import Qq /-! The `tauto` tactic. diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean index f5304c846f28b9..60ce419e206fa0 100644 --- a/Mathlib/Tactic/Widget/Calc.lean +++ b/Mathlib/Tactic/Widget/Calc.lean @@ -10,8 +10,8 @@ public meta import Lean.Elab.Tactic.Calc public meta import Lean.Meta.Tactic.TryThis public meta import Mathlib.Data.String.Defs public meta import Mathlib.Tactic.Widget.SelectPanelUtils -public import Mathlib.Tactic.Widget.SelectPanelUtils public meta import ProofWidgets.Component.OfRpcMethod +public import Mathlib.Tactic.Widget.SelectPanelUtils meta import ProofWidgets.Component.Basic diff --git a/Mathlib/Tactic/Widget/CommDiag.lean b/Mathlib/Tactic/Widget/CommDiag.lean index ae66cb381c6276..44159eee5c043c 100644 --- a/Mathlib/Tactic/Widget/CommDiag.lean +++ b/Mathlib/Tactic/Widget/CommDiag.lean @@ -6,9 +6,9 @@ Authors: Wojciech Nawrocki module public meta import Mathlib.Tactic.ToDual -public import Mathlib.CategoryTheory.Category.Basic public meta import ProofWidgets.Component.PenroseDiagram public meta import ProofWidgets.Presentation.Expr +public import Mathlib.CategoryTheory.Category.Basic /-! This module defines tactic/meta infrastructure for displaying commutative diagrams in the infoview. -/ diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean index 4a52fd8f2601c6..fad0aa47193527 100644 --- a/Mathlib/Tactic/Widget/Conv.lean +++ b/Mathlib/Tactic/Widget/Conv.lean @@ -6,8 +6,8 @@ Authors: Robin Böhne, Wojciech Nawrocki, Patrick Massot, Aaron Liu module public meta import Lean.PrettyPrinter.Delaborator.Builtins -public meta import ProofWidgets.Component.Basic public meta import Mathlib.Lean.Name +public meta import ProofWidgets.Component.Basic public import Mathlib.Tactic.Widget.SelectPanelUtils import ProofWidgets.Component.Basic diff --git a/Mathlib/Tactic/Widget/LibraryRewrite.lean b/Mathlib/Tactic/Widget/LibraryRewrite.lean index 6f743cecfef83f..37a936a18a2a77 100644 --- a/Mathlib/Tactic/Widget/LibraryRewrite.lean +++ b/Mathlib/Tactic/Widget/LibraryRewrite.lean @@ -9,11 +9,11 @@ public meta import Mathlib.Lean.GoalsLocation public meta import Mathlib.Lean.Meta.KAbstractPositions public meta import Mathlib.Lean.Meta.RefinedDiscrTree public meta import Mathlib.Tactic.Widget.SelectPanelUtils -public import Mathlib.Tactic.Widget.SelectPanelUtils public meta import ProofWidgets.Component.FilterDetails +public import Mathlib.Tactic.Widget.SelectPanelUtils -import Mathlib.Tactic.NthRewrite meta import ProofWidgets.Component.OfRpcMethod +import Mathlib.Tactic.NthRewrite /-! # Point & click library rewriting diff --git a/Mathlib/Tactic/Widget/SelectPanelUtils.lean b/Mathlib/Tactic/Widget/SelectPanelUtils.lean index 05cfa128897b6e..f7bc73c81952a5 100644 --- a/Mathlib/Tactic/Widget/SelectPanelUtils.lean +++ b/Mathlib/Tactic/Widget/SelectPanelUtils.lean @@ -7,9 +7,9 @@ module public meta import Lean.Meta.ExprLens public meta import Mathlib.Tactic.Widget.SelectInsertParamsClass -public import Mathlib.Tactic.Widget.SelectInsertParamsClass public meta import ProofWidgets.Component.MakeEditLink public meta import ProofWidgets.Data.Html +public import Mathlib.Tactic.Widget.SelectInsertParamsClass /-! # Selection panel utilities diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean index bd387ba0f92fc7..19ebe070a4bcc3 100644 --- a/Mathlib/Tactic/Widget/StringDiagram.lean +++ b/Mathlib/Tactic/Widget/StringDiagram.lean @@ -7,12 +7,12 @@ module public meta import Mathlib.Data.List.Defs public meta import Mathlib.Tactic.CategoryTheory.Coherence.Normalize +public meta import ProofWidgets.Component.HtmlDisplay public meta import ProofWidgets.Component.Panel.Basic public meta import ProofWidgets.Component.PenroseDiagram +public meta import ProofWidgets.Presentation.Expr public import Mathlib.Tactic.CategoryTheory.Bicategory.Normalize public import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize -public meta import ProofWidgets.Component.HtmlDisplay -public meta import ProofWidgets.Presentation.Expr /-! # String Diagram Widget diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean index 91defa79e9431f..6d9d3e30b0b9c3 100644 --- a/Mathlib/Util/AtomM.lean +++ b/Mathlib/Util/AtomM.lean @@ -6,8 +6,8 @@ Authors: Mario Carneiro module public meta import Lean.Meta.Tactic.Simp.Types -public import Mathlib.Init public meta import Qq +public import Mathlib.Init meta import Qq.Typ diff --git a/Mathlib/Util/Notation3.lean b/Mathlib/Util/Notation3.lean index 60f8c024a325f2..811d9d457d1f7b 100644 --- a/Mathlib/Util/Notation3.lean +++ b/Mathlib/Util/Notation3.lean @@ -6,13 +6,13 @@ Authors: Mario Carneiro, Kyle Miller module public meta import Batteries.Lean.Syntax +public meta import Lean.Elab.AuxDef public meta import Lean.Elab.MacroArgUtil public meta import Lean.PrettyPrinter.Delaborator -- shake: keep (dependency of elaborator output) public meta import Lean.PrettyPrinter.Delaborator.Builtins public meta import Mathlib.Lean.PrettyPrinter.Delaborator public import Batteries.Linter.UnreachableTactic public import Batteries.Util.ExtendedBinder -public meta import Lean.Elab.AuxDef public import Mathlib.Lean.Elab.Term public import Mathlib.Tactic.ScopedNS diff --git a/Mathlib/Util/PrintSorries.lean b/Mathlib/Util/PrintSorries.lean index 420d42d16753af..8f5751e98ab657 100644 --- a/Mathlib/Util/PrintSorries.lean +++ b/Mathlib/Util/PrintSorries.lean @@ -6,8 +6,8 @@ Authors: Henrik Böving, Yaël Dillies, Kyle Miller module public meta import Lean.Elab.Command -public meta import Mathlib.Lean.Name public meta import Lean.Meta.Sorry +public meta import Mathlib.Lean.Name /-! # Tracking uses of `sorry` diff --git a/Mathlib/Util/Qq.lean b/Mathlib/Util/Qq.lean index 1edbcb3c15451e..47e12199de3e4e 100644 --- a/Mathlib/Util/Qq.lean +++ b/Mathlib/Util/Qq.lean @@ -5,8 +5,8 @@ Authors: Kim Morrison, Alex J. Best, Yaël Dillies -/ module -public import Qq public import Lean.Meta.Tactic.Assumption +public import Qq import Mathlib.Init import Qq.Typ diff --git a/Mathlib/Util/SynthesizeUsing.lean b/Mathlib/Util/SynthesizeUsing.lean index ed14af46d2d409..f1651a66eda3ed 100644 --- a/Mathlib/Util/SynthesizeUsing.lean +++ b/Mathlib/Util/SynthesizeUsing.lean @@ -8,8 +8,8 @@ module public meta import Lean.Elab.Tactic.Basic public meta import Qq -import Mathlib.Init meta import Qq.Typ +import Mathlib.Init /-! # `SynthesizeUsing` diff --git a/MathlibTest/Linter/Header/ImportFormat.lean b/MathlibTest/Linter/Header/ImportFormat.lean new file mode 100644 index 00000000000000..ad652d73034aec --- /dev/null +++ b/MathlibTest/Linter/Header/ImportFormat.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2026 Thomas R. Murrills. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas R. Murrills +-/ +module + +import Mathlib.Init +meta import Mathlib.Init + + + public meta import Mathlib.Init + +public import Mathlib.Init +import Lean.Elab.Command + +/-- +warning: Imports can be reformatted: + i̵m̵p̵o̵r̵t̵ ̵M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵p̲u̲b̲l̲i̲c̲ meta import Mathlib.Init + public i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲ + ̲ + ̲meta ̵ ̵import Mathlib.Init + p̵u̵b̵l̵i̵c̵ ̵import M̵a̵t̵h̵l̵i̵b̵.̵I̵n̵i̵t̵ + ̵i̵m̵p̵o̵r̵t̵ ̵Lean.Elab.Command + ̲i̲m̲p̲o̲r̲t̲ ̲M̲a̲t̲h̲l̲i̲b̲.̲I̲n̲i̲t̲ + +Note: This linter can be disabled by writing `set_option linter.style.header.imports false` just after the import block. +-/ +#guard_msgs in +set_option linter.style.header true in +/-! -/ diff --git a/MathlibTest/Linter/Header/ImportFormatOff.lean b/MathlibTest/Linter/Header/ImportFormatOff.lean new file mode 100644 index 00000000000000..24db04cb4eb31f --- /dev/null +++ b/MathlibTest/Linter/Header/ImportFormatOff.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 Thomas R. Murrills. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas R. Murrills +-/ +module + +import Mathlib.Init +meta import Mathlib.Init + + + public meta import Mathlib.Init + +public import Mathlib.Init +import Lean.Elab.Command + +set_option linter.style.header.imports false + +#guard_msgs in +set_option linter.style.header true in +/-! -/