chore(Tactic/Linters): remove public section

Mathlib/Tactic/Linter/CommandRanges.lean

@@ -20,7 +20,7 @@ This linter is strictly tied to the `#clear_deprecations` command in
 `Mathlib/Tactic/Linter/FindDeprecations.lean`.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
@@ -38,7 +38,7 @@ Thus, assuming that there has been no tampering with positions/synthetic syntax,
 if the current command is followed by another command, then `trailing` for the previous command
 coincides with `start` of the following.
 -/
-register_option linter.commandRanges : Bool := {
+public register_option linter.commandRanges : Bool := {
   defValue := false
   descr := "enable the commandRanges linter"
 }

Mathlib/Tactic/Linter/CommandStart.lean

@@ -15,7 +15,7 @@ The `commandStart` linter emits a warning if
 * or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
@@ -35,14 +35,14 @@ as opposed to
 example (a: Nat) {R:Type}  [Add  R] : <not linted part>
 ```
 -/
-register_option linter.style.commandStart : Bool := {
+public register_option linter.style.commandStart : Bool := {
   defValue := false
   descr := "enable the commandStart linter"
 }
 
 /-- If the `linter.style.commandStart.verbose` option is `true`, the `commandStart` linter
 reports some helpful diagnostic information. -/
-register_option linter.style.commandStart.verbose : Bool := {
+public register_option linter.style.commandStart.verbose : Bool := {
   defValue := false
   descr := "enable the commandStart linter"
 }
@@ -193,6 +193,7 @@ def parallelScanAux (as : Array FormatError) (L M : String) : Array FormatError
       pushFormatError as (mkFormatError ls ms "Oh no! (Unreachable?)")
 
 @[inherit_doc parallelScanAux]
+public -- for use in unit tests only
 def parallelScan (src fmt : String) : Array FormatError :=
   parallelScanAux ∅ src fmt
 
@@ -289,7 +290,7 @@ to avoid cutting into "words".
 
 *Note*. `start` is the number of characters *from the right* where our focus is!
 -/
-def mkWindow (orig : String) (start ctx : Nat) : String :=
+public def mkWindow (orig : String) (start ctx : Nat) : String :=
   let head := orig.dropRight (start + 1) -- `orig`, up to one character before the discrepancy
   let middle := orig.takeRight (start + 1)
   let headCtx := head.takeRightWhile (!·.isWhitespace)

Mathlib/Tactic/Linter/DeprecatedModule.lean

@@ -27,7 +27,7 @@ This triggers the `deprecated.module` linter to notify every file with `import A
 to instead import the *direct imports* of `A`, that is `B, ..., Z`.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
@@ -39,7 +39,7 @@ is imported.
 The default value is `true`, since this linter is designed to warn projects downstream of `Mathlib`
 of refactors and deprecations in `Mathlib` itself.
 -/
-register_option linter.deprecated.module : Bool := {
+public register_option linter.deprecated.module : Bool := {
   defValue := true
   descr := "enable the `deprecated.module` linter"
 }
@@ -52,7 +52,7 @@ Defines the `deprecatedModuleExt` extension for adding a `HashSet` of triples of
 
 to the environment.
 -/
-initialize deprecatedModuleExt :
+public initialize deprecatedModuleExt :
     SimplePersistentEnvExtension
       (Name × Array Name × Option String) (Std.HashSet (Name × Array Name × Option String)) ←
   registerSimplePersistentEnvExtension {

Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean

@@ -35,7 +35,7 @@ This linter is an incentive to discourage uses of such deprecated syntax, withou
 It is not inherently limited to tactics.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
@@ -49,7 +49,7 @@ differently. This means that they are not completely interchangeable, nor can on
 replace another. However, `refine` and `apply` are more readable and (heuristically) tend to be
 more efficient on average.
 -/
-register_option linter.style.refine : Bool := {
+public register_option linter.style.refine : Bool := {
   defValue := false
   descr := "enable the refine linter"
 }
@@ -59,7 +59,7 @@ the `cases'` tactic, which is a backward-compatible version of Lean 3's `cases`
 Unlike `obtain`, `rcases` and Lean 4's `cases`, variables introduced by `cases'` are not
 required to be separated by case, which hinders readability.
 -/
-register_option linter.style.cases : Bool := {
+public register_option linter.style.cases : Bool := {
   defValue := false
   descr := "enable the cases linter"
 }
@@ -69,14 +69,14 @@ the `induction'` tactic, which is a backward-compatible version of Lean 3's `ind
 Unlike Lean 4's `induction`, variables introduced by `induction'` are not
 required to be separated by case, which hinders readability.
 -/
-register_option linter.style.induction : Bool := {
+public register_option linter.style.induction : Bool := {
   defValue := false
   descr := "enable the induction linter"
 }
 
 /-- The option `linter.style.admit` of the deprecated syntax linter flags usages of
 the `admit` tactic, which is a synonym for the much more common `sorry`. -/
-register_option linter.style.admit : Bool := {
+public register_option linter.style.admit : Bool := {
   defValue := false
   descr := "enable the admit linter"
 }
@@ -86,7 +86,7 @@ the `native_decide` tactic, which is disallowed in mathlib. -/
 -- Note: this linter is purely for user information. Running `lean4checker` in CI catches *any*
 -- additional axioms that are introduced (not just `ofReduceBool`): the point of this check is to
 -- alert the user quickly, not to be airtight.
-register_option linter.style.nativeDecide : Bool := {
+public register_option linter.style.nativeDecide : Bool := {
   defValue := false
   descr := "enable the nativeDecide linter"
 }
@@ -97,7 +97,7 @@ the reason for the modification of the `maxHeartbeats`.
 
 This includes `set_option maxHeartbeats n in` and `set_option synthInstance.maxHeartbeats n in`.
 -/
-register_option linter.style.maxHeartbeats : Bool := {
+public register_option linter.style.maxHeartbeats : Bool := {
   defValue := false
   descr := "enable the maxHeartbeats linter"
 }
@@ -235,3 +235,5 @@ def deprecatedSyntaxLinter : Linter where run stx := do
 initialize addLinter deprecatedSyntaxLinter
 
 end Mathlib.Linter.Style
+
+end

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -17,16 +17,17 @@ independent. By specifying that one directory does not import from another, we c
 modularity of Mathlib.
 -/
 
-public meta section
+meta section
 
--- XXX: is there a better long-time place for this
+-- XXX: is there a better long-time place for this?
 /-- Parse all imports in a text file at `path` and return just their names:
 this is just a thin wrapper around `Lean.parseImports'`.
 Omit `Init` (which is part of the prelude). -/
-def findImports (path : System.FilePath) : IO (Array Lean.Name) := do
+public def findImports (path : System.FilePath) : IO (Array Lean.Name) := do
   return (← Lean.parseImports' (← IO.FS.readFile path) path.toString).imports
     |>.map (fun imp ↦ imp.module) |>.erase `Init
 
+-- XXX: is there a better location for these?
 /-- Find the longest prefix of `n` such that `f` returns `some` (or return `none` otherwise). -/
 def Lean.Name.findPrefix {α} (f : Name → Option α) (n : Name) : Option α := do
   f n <|> match n with
@@ -61,6 +62,7 @@ current module.
 
 The path only contains the intermediate steps: it excludes `imported` and the current module.
 -/
+public
 def Lean.Environment.importPath (env : Environment) (imported : Name) : Array Name := Id.run do
   let mut result := #[]
   let modData := env.header.moduleData
@@ -81,7 +83,7 @@ open Lean Elab Command Linter
 The `directoryDependency` linter detects imports between directories that are supposed to be
 independent. If this is the case, it emits a warning.
 -/
-register_option linter.directoryDependency : Bool := {
+public register_option linter.directoryDependency : Bool := {
   defValue := true
   descr := "enable the directoryDependency linter"
 }
@@ -96,7 +98,8 @@ prefixes `n₁'` of `n₁` and `n₂'` of `n₂` such that `n₁' R n₂'`.
 The current implementation is a `NameMap` of `NameSet`s, testing each prefix of `n₁` and `n₂` in
 turn. This can probably be optimized.
 -/
-@[expose] def NamePrefixRel := NameMap NameSet
+--@[expose]
+def NamePrefixRel := NameMap NameSet
 
 namespace NamePrefixRel
 
@@ -639,7 +642,7 @@ private def checkBlocklist (env : Environment) (mainModule : Name) (imports : Ar
   | none => none
 
 @[inherit_doc Mathlib.Linter.linter.directoryDependency]
-def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageData) := do
+public def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageData) := do
   unless Linter.getLinterValue linter.directoryDependency (← Linter.getLinterOptions) do
     return #[]
   let env ← getEnv

Mathlib/Tactic/Linter/DocPrime.lean

@@ -20,7 +20,7 @@ to an unprimed version of that declaration, or an explanation as to why no bette
 is possible.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
@@ -33,7 +33,7 @@ name ends with a `'`.
 The file `scripts/nolints_prime_decls.txt` contains a list of temporary exceptions to this linter.
 This list should not be appended to, and become emptied over time.
 -/
-register_option linter.docPrime : Bool := {
+public register_option linter.docPrime : Bool := {
   defValue := false
   descr := "enable the docPrime linter"
 }

Mathlib/Tactic/Linter/DocString.lean

@@ -13,7 +13,7 @@ public meta import Mathlib.Tactic.Linter.Header
 The "DocString" linter validates style conventions regarding doc-string formatting.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
@@ -22,15 +22,15 @@ namespace Mathlib.Linter
 /--
 The "DocString" linter validates style conventions regarding doc-string formatting.
 -/
-register_option linter.style.docString : Bool := {
+public register_option linter.style.docString : Bool := {
   defValue := false
   descr := "enable the style.docString linter"
 }
 
 /--
 The "empty doc string" warns on empty doc-strings.
 -/
-register_option linter.style.docString.empty : Bool := {
+public register_option linter.style.docString.empty : Bool := {
   defValue := true
   descr := "enable the style.docString.empty linter"
 }
@@ -39,7 +39,7 @@ register_option linter.style.docString.empty : Bool := {
 Extract all `declModifiers` from the input syntax. We later extract the `docstring` from it,
 but we avoid extracting directly the `docComment` node, to skip `#adaptation_note`s.
 -/
-def getDeclModifiers : Syntax → Array Syntax
+public def getDeclModifiers : Syntax → Array Syntax
   | s@(.node _ kind args) =>
     (if kind == ``Parser.Command.declModifiers then #[s] else #[]) ++ args.flatMap getDeclModifiers
   | _ => #[]

Mathlib/Tactic/Linter/FindDeprecations.lean

@@ -19,7 +19,7 @@ ending with `date₂`.
 See the doc-string for the command for more information.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command
 
@@ -152,6 +152,7 @@ def deprecatedHashMap (oldDate newDate : String) :
 * The command makes the assumption that `rgs` is *sorted*.
 * The command removes all consecutive whitespace following the end of each range.
 -/
+public -- for use in unit tests, but perhaps useful more broadly
 def removeRanges (file : String) (rgs : Array Lean.Syntax.Range) : String := Id.run do
   let mut curr : String.Pos.Raw := 0
   let mut fileSubstring := file.toSubstring
@@ -185,6 +186,7 @@ It makes the assumption that there is a unique `: [` substring and then retrieve
 Note that this is the output of `Mathlib.Linter.CommandRanges.commandRangesLinter`
 that the script here is parsing.
 -/
+public -- for use in unit tests, but perhaps useful more broadly
 def parseLine (line : String) : Option (List String.Pos.Raw) :=
   match (line.dropRight 1).splitOn ": [" with
   | [_, rest] =>

Mathlib/Tactic/Linter/FlexibleLinter.lean

@@ -91,14 +91,14 @@ We then propagate all the `FVarId`s that were present in the "before" goals to t
 while leaving untouched the ones in the "inert" goals.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
 namespace Mathlib.Linter
 
 /-- The flexible linter makes sure that "rigid" tactics do not follow "flexible" tactics. -/
-register_option linter.flexible : Bool := {
+public register_option linter.flexible : Bool := {
   defValue := false
   descr := "enable the flexible linter"
 }
@@ -110,6 +110,7 @@ The prototypical flexible tactic is `simp`.
 The prototypical non-flexible tactic `rw`.
 `simp only` is also non-flexible. -/
 --  TODO: adding more entries here, allows to consider more tactics to be flexible
+public -- for testing
 def flexible? : Syntax → Bool
   | .node _ ``Lean.Parser.Tactic.simp #[_, _, _, only?, _, _] => only?[0].getAtomVal != "only"
   | .node _ ``Lean.Parser.Tactic.simpAll #[_, _, _, only?, _] => only?[0].getAtomVal != "only"
@@ -196,7 +197,7 @@ The function is used to extract "location" information about `stx`: either expli
 
 Whether or not what this function extracts really is a location will be determined by the linter
 using data embedded in the `InfoTree`s. -/
-partial
+public partial -- public for use in unit testing
 def toStained : Syntax → Std.HashSet Stained
   | .node _ _ arg => (arg.map toStained).foldl (.union) {}
   | .ident _ _ val _ => {.name val}

Mathlib/Tactic/Linter/GlobalAttributeIn.lean

@@ -77,15 +77,15 @@ example : False := by simp
 ```
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
 namespace Mathlib.Linter
 
 /-- Lint on any occurrence of `attribute [...] name in` which is not `local` or `scoped`:
 these are a footgun, as the attribute is applied *globally* (despite the `in`). -/
-register_option linter.globalAttributeIn : Bool := {
+public register_option linter.globalAttributeIn : Bool := {
   defValue := true
   descr := "enable the globalAttributeIn linter"
 }

Mathlib/Tactic/Linter/HashCommandLinter.lean

@@ -23,7 +23,7 @@ Most of them are noisy and get picked up anyway by CI, but even the quiet ones a
 outlive their in-development status.
 -/
 
-public meta section
+meta section
 
 namespace Mathlib.Linter
 
@@ -32,7 +32,7 @@ The linter emits a warning on any command beginning with `#` that itself emits n
 For example, `#guard true` and `#check_tactic True ~> True by skip` trigger a message.
 There is a list of silent `#`-command that are allowed.
 -/
-register_option linter.hashCommand : Bool := {
+public register_option linter.hashCommand : Bool := {
   defValue := false
   descr := "enable the `#`-command linter"
 }

Mathlib/Tactic/Linter/HaveLetLinter.lean

@@ -27,7 +27,7 @@ TODO:
   should the linter act on them as well?
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Meta
 
@@ -42,7 +42,7 @@ There are three settings:
 
 The default value is `1`.
 -/
-register_option linter.haveLet : Nat := {
+public register_option linter.haveLet : Nat := {
   defValue := 0
   descr := "enable the `have` vs `let` linter:\n\
             * 0 -- inactive;\n\
@@ -87,7 +87,7 @@ def toFormat_propTypes (ctx : ContextInfo) (lc : LocalContext) (es : Array (Expr
 
 /-- returns the `have` syntax whose corresponding hypothesis does not have Type `Prop` and
 also a `Format`ted version of the corresponding Type. -/
-partial
+public partial
 def nonPropHaves : InfoTree → CommandElabM (Array (Syntax × Format)) :=
   InfoTree.foldInfoM (init := #[]) fun ctx info args => return args ++ (← do
     let .ofTacticInfo i := info | return #[]