chore: always include comment when importing header linter explicitly (leanprover-community#40729)

thorimur · bryangingechen · commit b6b3fc845cce · 2026-06-21T20:54:34.000-04:00
This PR makes sure we always includes the comment ``` -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. ``` whenever `Mathlib.Tactic.Linter.Header` is imported explicitly. Some files already had this comment, and this PR just makes sure all of them do. We also normalize whitespace in adjacent `shake` annotations while we're at it. We could check for this in lint-style, but it would be easier after leanprover-community#40347.
diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean
@@ -11,7 +11,7 @@ public import Lean.Meta.TryThis
 public import Batteries.Tactic.Lint.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
+import Mathlib.Tactic.Linter.Header  -- shake: keep
 public import Batteries.Tactic.Lint.Basic
 import Lean.Elab.Term.TermElabM
 
diff --git a/Mathlib/Lean/Environment.lean b/Mathlib/Lean/Environment.lean
@@ -8,7 +8,7 @@ module
 public import Lean.Environment
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
-import Mathlib.Tactic.Linter.Header  --shake: keep
+import Mathlib.Tactic.Linter.Header  -- shake: keep
 
 /-!
 # Additional utilities for `Lean.Environment`
diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
@@ -8,7 +8,7 @@ module
 
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
-import Mathlib.Tactic.Linter.Header  --shake: keep
+import Mathlib.Tactic.Linter.Header  -- shake: keep
 public import Lean.Meta.AppBuilder
 public import Lean.Meta.Match.MatcherInfo
 public import Lean.Meta.Transform
diff --git a/Mathlib/Tactic/Linter/AuxLemma.lean b/Mathlib/Tactic/Linter/AuxLemma.lean
@@ -6,6 +6,8 @@ Authors: Kim Morrison
 module
 
 public meta import Lean.Elab.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
 
 /-!
diff --git a/Mathlib/Tactic/Linter/DocString.lean b/Mathlib/Tactic/Linter/DocString.lean
@@ -5,6 +5,8 @@ Authors: Michael Rothgang, Damiano Testa
 -/
 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 Std.Data.Iterators.Combinators.Zip
 public import Lean.Parser.Command
diff --git a/Mathlib/Tactic/Linter/EmptyLine.lean b/Mathlib/Tactic/Linter/EmptyLine.lean
@@ -5,6 +5,9 @@ Authors: Damiano Testa
 -/
 
 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 import Lean.Parser.Command
 
diff --git a/Mathlib/Tactic/Linter/FlexibleLinter.lean b/Mathlib/Tactic/Linter/FlexibleLinter.lean
@@ -9,6 +9,8 @@ public meta import Lean.Elab.Command
 public meta import Lean.Elab.Tactic.Simp
 public meta import Lean.Meta.Tactic.TryThis
 public meta import Lean.Server.InfoUtils
+-- 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 Lean.Parser.Term
 
diff --git a/Mathlib/Tactic/Linter/TacticDocumentation.lean b/Mathlib/Tactic/Linter/TacticDocumentation.lean
@@ -7,6 +7,8 @@ module
 
 public meta import Lean.Elab.Tactic.Doc
 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 Lean.Elab.Tactic.Doc
diff --git a/Mathlib/Tactic/Linter/UnusedInstancesInType.lean b/Mathlib/Tactic/Linter/UnusedInstancesInType.lean
@@ -11,7 +11,7 @@ public meta import Mathlib.Lean.Elab.InfoTree
 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 Mathlib.Tactic.Linter.Header  -- shake: keep
 public import Batteries.Tactic.Lint.Basic
 public import Batteries.Tactic.Lint.Misc
 
diff --git a/Mathlib/Tactic/Linter/Whitespace.lean b/Mathlib/Tactic/Linter/Whitespace.lean
@@ -5,6 +5,8 @@ Authors: Damiano Testa
 -/
 module
 
+-- 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/TypeStar.lean b/Mathlib/Tactic/TypeStar.lean
@@ -7,7 +7,7 @@ module
 
 -- 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 Mathlib.Tactic.Linter.Header  -- shake: keep
 
 /-!
 # Support for `Sort*` and `Type*`.
diff --git a/Mathlib/Util/ParseCommand.lean b/Mathlib/Util/ParseCommand.lean
@@ -8,7 +8,7 @@ module
 public meta import Lean.Elab.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 Mathlib.Tactic.Linter.Header  -- shake: keep
 
 /-!
 # `#parse` -- a command to parse text and log outputs
