diff --git a/Mathlib/Tactic/Linter/CommandRanges.lean b/Mathlib/Tactic/Linter/CommandRanges.lean
index 095ab3db25d6df..99a7689079de08 100644
--- a/Mathlib/Tactic/Linter/CommandRanges.lean
+++ b/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"
 }
diff --git a/Mathlib/Tactic/Linter/CommandStart.lean b/Mathlib/Tactic/Linter/CommandStart.lean
index 59fd3453552de2..9d7b2aa6a8a9c5 100644
--- a/Mathlib/Tactic/Linter/CommandStart.lean
+++ b/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)
diff --git a/Mathlib/Tactic/Linter/DeprecatedModule.lean b/Mathlib/Tactic/Linter/DeprecatedModule.lean
index 8240c2432e11fa..4cfa00c79e6b66 100644
--- a/Mathlib/Tactic/Linter/DeprecatedModule.lean
+++ b/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 {
diff --git a/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean b/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
index 7cf21ca9fe25cb..9ea31895d55e2b 100644
--- a/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
+++ b/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
diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean
index 4bf868df0b6905..2653e255949b17 100644
--- a/Mathlib/Tactic/Linter/DirectoryDependency.lean
+++ b/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
diff --git a/Mathlib/Tactic/Linter/DocPrime.lean b/Mathlib/Tactic/Linter/DocPrime.lean
index fd76c77a4ab75a..03b32da57c3d18 100644
--- a/Mathlib/Tactic/Linter/DocPrime.lean
+++ b/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"
 }
diff --git a/Mathlib/Tactic/Linter/DocString.lean b/Mathlib/Tactic/Linter/DocString.lean
index 6082eb27e393a0..2c7650ac9d4c5d 100644
--- a/Mathlib/Tactic/Linter/DocString.lean
+++ b/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,7 +22,7 @@ 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"
 }
@@ -30,7 +30,7 @@ register_option linter.style.docString : Bool := {
 /--
 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
   | _ => #[]
diff --git a/Mathlib/Tactic/Linter/FindDeprecations.lean b/Mathlib/Tactic/Linter/FindDeprecations.lean
index 5a922e21554729..abdc9d4fd7ef1b 100644
--- a/Mathlib/Tactic/Linter/FindDeprecations.lean
+++ b/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] =>
diff --git a/Mathlib/Tactic/Linter/FlexibleLinter.lean b/Mathlib/Tactic/Linter/FlexibleLinter.lean
index cc7dd210b83987..728eb259ce5578 100644
--- a/Mathlib/Tactic/Linter/FlexibleLinter.lean
+++ b/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}
diff --git a/Mathlib/Tactic/Linter/GlobalAttributeIn.lean b/Mathlib/Tactic/Linter/GlobalAttributeIn.lean
index bfec9739422818..58d18dbf46301a 100644
--- a/Mathlib/Tactic/Linter/GlobalAttributeIn.lean
+++ b/Mathlib/Tactic/Linter/GlobalAttributeIn.lean
@@ -77,7 +77,7 @@ example : False := by simp
 ```
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
@@ -85,7 +85,7 @@ 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"
 }
diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean
index 99789a4dc0dc75..b3be24f24a5fba 100644
--- a/Mathlib/Tactic/Linter/HashCommandLinter.lean
+++ b/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"
 }
diff --git a/Mathlib/Tactic/Linter/HaveLetLinter.lean b/Mathlib/Tactic/Linter/HaveLetLinter.lean
index 0ebd88a5d02687..f0d0c688472e24 100644
--- a/Mathlib/Tactic/Linter/HaveLetLinter.lean
+++ b/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 #[]
diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index 03a3f104977823..13e52d71433156 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -50,7 +50,7 @@ could arise from this part and also flag that the file should contain a module d
 the `import` statements.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
@@ -76,8 +76,7 @@ It returns the array of all `import` identifiers in `s`. -/
 --   to Mathlib.Init (where this linter is imported)
 -- - that function does not return the Syntax corresponding to each import,
 --   which we use to log more precise warnings.
-partial
-def getImportIds (s : Syntax) : Array Syntax :=
+public partial def getImportIds (s : Syntax) : Array Syntax :=
   let rest : Array Syntax := (s.getArgs.map getImportIds).flatten
   if let `(Lean.Parser.Module.import| import $n) := s then
     rest.push n
@@ -160,7 +159,7 @@ The linter checks that
 * the remainder of the string begins with `Authors: `, does not end with `.` and
   contains no ` and ` nor a double space, except possibly after a line break.
 -/
-def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) := Id.run do
+public def copyrightHeaderChecks (copyright : String) : Array (Syntax × String) := Id.run do
   -- First, we merge lines ending in `,`: two spaces after the line-break are ok,
   -- but so is only one or none.  We take care of *not* adding more consecutive spaces, though.
   -- This is to allow the copyright or authors' lines to span several lines.
@@ -269,7 +268,7 @@ It emits a warning if
 
 The linter allows `import`-only files and does not require a copyright statement in `Mathlib.Init`.
 -/
-register_option linter.style.header : Bool := {
+public register_option linter.style.header : Bool := {
   defValue := false
   descr := "enable the header style linter"
 }
diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean
index 5cb2f629793ff7..dbbf08f6703f33 100644
--- a/Mathlib/Tactic/Linter/Lint.lean
+++ b/Mathlib/Tactic/Linter/Lint.lean
@@ -17,7 +17,7 @@ which concern the *behaviour* of the linted code, and not issues of code style o
 Perhaps these should be moved to Batteries in the future.
 -/
 
-public meta section
+meta section
 
 namespace Batteries.Tactic.Lint
 open Lean Meta
@@ -25,7 +25,7 @@ open Lean Meta
 /--
 Linter that checks whether a structure should be in Prop.
 -/
-@[env_linter] def structureInType : Linter where
+@[env_linter] public def structureInType : Linter where
   noErrorsFound := "no structures that should be in Prop found."
   errorsFound := "FOUND STRUCTURES THAT SHOULD BE IN PROP."
   test declName := do
@@ -42,7 +42,7 @@ Linter that checks whether a structure should be in Prop.
     return m!"all fields are propositional but the structure isn't."
 
 /-- Linter that check that all `deprecated` tags come with `since` dates. -/
-@[env_linter] def deprecatedNoSince : Linter where
+@[env_linter] public def deprecatedNoSince : Linter where
   noErrorsFound := "no `deprecated` tags without `since` dates."
   errorsFound := "FOUND `deprecated` tags without `since` dates."
   test declName := do
@@ -74,7 +74,7 @@ For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.
 This linter will not detect duplication in namespaces of autogenerated declarations
 (other than the one whose `declId` is present in the source declaration).
 -/
-register_option linter.dupNamespace : Bool := {
+public register_option linter.dupNamespace : Bool := {
   defValue := true
   descr := "enable the duplicated namespace linter"
 }
diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index add8f6cc95c9fd..a9558dde7dcd4b 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -20,7 +20,7 @@ It also works incrementally, accumulating increasing import information.
 This is better suited, for instance, to split files.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
@@ -70,7 +70,7 @@ Another important difference is that the `minImports` *linter* starts counting i
 where the option is set to `true` *downwards*, whereas the `#min_imports` *command* looks at the
 imports needed from the command *upwards*.
 -/
-register_option linter.minImports : Bool := {
+public register_option linter.minImports : Bool := {
   defValue := false
   descr := "enable the minImports linter"
 }
@@ -79,7 +79,7 @@ register_option linter.minImports : Bool := {
 change in number of imports, when it reports import changes.
 Setting this option to `false` helps with test stability.
 -/
-register_option linter.minImports.increases : Bool := {
+public register_option linter.minImports.increases : Bool := {
   defValue := true
   descr := "enable reporting increase-size change in the minImports linter"
 }
diff --git a/Mathlib/Tactic/Linter/Multigoal.lean b/Mathlib/Tactic/Linter/Multigoal.lean
index 8462df1518201d..501b405456daff 100644
--- a/Mathlib/Tactic/Linter/Multigoal.lean
+++ b/Mathlib/Tactic/Linter/Multigoal.lean
@@ -39,14 +39,14 @@ TODO:
   Maybe revisit usages of `on_goal` and also nested `induction` and `cases`.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
 namespace Mathlib.Linter
 
 /-- The "multiGoal" linter emits a warning when there are multiple active goals. -/
-register_option linter.style.multiGoal : Bool := {
+public register_option linter.style.multiGoal : Bool := {
   defValue := false
   descr := "enable the multiGoal linter"
 }
diff --git a/Mathlib/Tactic/Linter/OldObtain.lean b/Mathlib/Tactic/Linter/OldObtain.lean
index 0383454f27aa35..791a586bf14601 100644
--- a/Mathlib/Tactic/Linter/OldObtain.lean
+++ b/Mathlib/Tactic/Linter/OldObtain.lean
@@ -50,7 +50,7 @@ case... but by now, the "old" syntax is not clearly better.)
 In the 30 replacements of the last PR, this occurred twice. In both cases, the `suffices` tactic
 could also be used, as was in fact clearer. -/
 
-public meta section
+meta section
 
 open Lean Elab Linter
 
@@ -65,7 +65,7 @@ def isObtainWithoutProof : Syntax → Bool
 
 /-- The `oldObtain` linter emits a warning upon uses of the "stream-of-consciousness" variants
 of the `obtain` tactic, i.e. with the proof postponed. -/
-register_option linter.oldObtain : Bool := {
+public register_option linter.oldObtain : Bool := {
   defValue := false
   descr := "enable the `oldObtain` linter"
 }
diff --git a/Mathlib/Tactic/Linter/PPRoundtrip.lean b/Mathlib/Tactic/Linter/PPRoundtrip.lean
index bc92cc2fb762dd..3549f556b63f9a 100644
--- a/Mathlib/Tactic/Linter/PPRoundtrip.lean
+++ b/Mathlib/Tactic/Linter/PPRoundtrip.lean
@@ -15,7 +15,7 @@ The "ppRoundtrip" linter emits a warning when the syntax of a command differs su
 from the pretty-printed version of itself.
 -/
 
-public meta section
+meta section
 open Lean Elab Command Linter
 
 namespace Mathlib.Linter
@@ -29,7 +29,7 @@ However, it may not always be successful.
 It also prints both the source code and the "expected code" in a 5-character radius from
 the first difference.
 -/
-register_option linter.ppRoundtrip : Bool := {
+public register_option linter.ppRoundtrip : Bool := {
   defValue := false
   descr := "enable the ppRoundtrip linter"
 }
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index 4d5a03ae9b163e..11d396bf307d1f 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -42,7 +42,7 @@ All of these linters are enabled in mathlib by default, but disabled globally
 since they enforce conventions which are inherently subjective.
 -/
 
-public meta section
+meta section
 
 open Lean Parser Elab Command Meta Linter
 
@@ -52,7 +52,7 @@ namespace Mathlib.Linter
 which sets a `pp`, `profiler` or `trace` option.
 It also warns on an option containing `maxHeartbeats`
 (as these should be scoped as `set_option ... in` instead). -/
-register_option linter.style.setOption : Bool := {
+public register_option linter.style.setOption : Bool := {
   defValue := false
   descr := "enable the `setOption` linter"
 }
@@ -69,7 +69,7 @@ def parseSetOption : Syntax → Option Name
   | _ => none
 
 /-- Whether a given piece of syntax is a `set_option` command, tactic or term. -/
-def isSetOption : Syntax → Bool :=
+public def isSetOption : Syntax → Bool :=
   fun stx ↦ parseSetOption stx matches some _name
 
 /-- The `setOption` linter: this lints any `set_option` command, term or tactic
@@ -126,7 +126,7 @@ open Lean Elab Command
 /-- The "missing end" linter emits a warning on non-closed `section`s and `namespace`s.
 It allows the "outermost" `noncomputable section` to be left open (whether or not it is named).
 -/
-register_option linter.style.missingEnd : Bool := {
+public register_option linter.style.missingEnd : Bool := {
   defValue := false
   descr := "enable the missing end linter"
 }
@@ -175,14 +175,14 @@ The `cdot` linter flags uses of the "cdot" `·` that are achieved by typing a ch
 different from `·`.
 For instance, a "plain" dot `.` is allowed syntax, but is flagged by the linter.
 It also flags "isolated cdots", i.e. when the `·` is on its own line. -/
-register_option linter.style.cdot : Bool := {
+public register_option linter.style.cdot : Bool := {
   defValue := false
   descr := "enable the `cdot` linter"
 }
 
 /-- `isCDot? stx` checks whether `stx` is a `Syntax` node corresponding to a `cdot` typed with
 the character `·`. -/
-def isCDot? : Syntax → Bool
+public def isCDot? : Syntax → Bool
   | .node _ ``cdotTk #[.node _ `patternIgnore #[.node _ _ #[.atom _ v]]] => v == "·"
   | .node _ ``Lean.Parser.Term.cdot #[.atom _ v, _] => v == "·"
   | _ => false
@@ -239,7 +239,7 @@ These are disallowed by the mathlib style guide, as using `<|` pairs better with
 
 /-- The `dollarSyntax` linter flags uses of `<|` that are achieved by typing `$`.
 These are disallowed by the mathlib style guide, as using `<|` pairs better with `|>`. -/
-register_option linter.style.dollarSyntax : Bool := {
+public register_option linter.style.dollarSyntax : Bool := {
   defValue := false
   descr := "enable the `dollarSyntax` linter"
 }
@@ -247,7 +247,7 @@ register_option linter.style.dollarSyntax : Bool := {
 namespace Style.dollarSyntax
 
 /-- `findDollarSyntax stx` extracts from `stx` the syntax nodes of `kind` `$`. -/
-partial
+public partial
 def findDollarSyntax : Syntax → Array Syntax
   | stx@(.node _ kind args) =>
     let dargs := (args.map findDollarSyntax).flatten
@@ -282,7 +282,7 @@ prefers the latter as it is considered more readable.
 The `lambdaSyntax` linter flags uses of the symbol `λ` to define anonymous functions.
 This is syntactically equivalent to the `fun` keyword; mathlib style prefers using the latter.
 -/
-register_option linter.style.lambdaSyntax : Bool := {
+public register_option linter.style.lambdaSyntax : Bool := {
   defValue := false
   descr := "enable the `lambdaSyntax` linter"
 }
@@ -291,7 +291,7 @@ namespace Style.lambdaSyntax
 
 /--
 `findLambdaSyntax stx` extracts from `stx` all syntax nodes of `kind` `Term.fun`. -/
-partial
+public partial
 def findLambdaSyntax : Syntax → Array Syntax
   | stx@(.node _ kind args) =>
     let dargs := (args.map findLambdaSyntax).flatten
@@ -329,13 +329,13 @@ The "longFile" linter emits a warning on files which are longer than a certain n
 If this option is set to `N` lines, the linter warns once a file has more than `N` lines.
 A value of `0` silences the linter entirely.
 -/
-register_option linter.style.longFile : Nat := {
+public register_option linter.style.longFile : Nat := {
   defValue := 0
   descr := "enable the longFile linter"
 }
 
 /-- The number of lines that the `longFile` linter considers the default. -/
-register_option linter.style.longFileDefValue : Nat := {
+public register_option linter.style.longFileDefValue : Nat := {
   defValue := 1500
   descr := "a soft upper bound on the number of lines of each file"
 }
@@ -406,7 +406,7 @@ end Style.longFile
 
 /-- The "longLine" linter emits a warning on lines longer than 100 characters.
 We allow lines containing URLs to be longer, though. -/
-register_option linter.style.longLine : Bool := {
+public register_option linter.style.longLine : Bool := {
   defValue := false
   descr := "enable the longLine linter"
 }
@@ -457,7 +457,7 @@ probably have been introduced by accident.
 **How to fix this?** Use single underscores to separate parts of a name, following standard naming
 conventions.
 -/
-register_option linter.style.nameCheck : Bool := {
+public register_option linter.style.nameCheck : Bool := {
   defValue := true
   descr := "enable the `nameCheck` linter"
 }
@@ -494,7 +494,7 @@ end Style.nameCheck
 scoped to a single declaration. A non-scoped `open Classical` can hide that some theorem statements
 would be better stated with explicit decidability statements.
 -/
-register_option linter.style.openClassical : Bool := {
+public register_option linter.style.openClassical : Bool := {
   defValue := false
   descr := "enable the openClassical linter"
 }
@@ -508,7 +508,7 @@ omitting any renamed or hidden items.
 This only checks independent `open` commands: for `open ... in ...` commands,
 this linter returns an empty array.
 -/
-def extractOpenNames : Syntax → Array (TSyntax `ident)
+public def extractOpenNames : Syntax → Array (TSyntax `ident)
   | `(command|$_ in $_) => #[] -- redundant, for clarity
   | `(command|open $decl:openDecl) => match decl with
     | `(openDecl| $arg hiding $_*)    => #[arg]
@@ -545,7 +545,7 @@ The "show" linter emits a warning if the `show` tactic changed the goal. `show`
 to indicate intermediate goal states for proof readability. When the goal is actually changed,
 `change` should be preferred.
 -/
-register_option linter.style.show : Bool := {
+public register_option linter.style.show : Bool := {
   defValue := false
   descr := "enable the show linter"
 }
diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 8c15c15fce4b47..ffff7d19bc57e7 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -13,7 +13,7 @@ public meta import Lake.Util.Casing
 -- benchmarked.
 set_option linter.style.header false
 
-public meta section
+meta section
 
 /-!
 ## Text-based linters
@@ -57,7 +57,7 @@ inductive StyleError where
 deriving BEq
 
 /-- How to format style errors -/
-inductive ErrorFormat
+public inductive ErrorFormat
   /-- Produce style error output aimed at humans: no error code, clickable file name -/
   | humanReadable : ErrorFormat
   /-- Produce an entry in the style-exceptions file: mention the error code, slightly uglier
@@ -199,7 +199,7 @@ abbrev TextbasedLinter := LinterOptions → Array String →
 section
 
 /-- Lint on any occurrences of the string "Adaptation note:" or variants thereof. -/
-register_option linter.adaptationNote : Bool := { defValue := true }
+public register_option linter.adaptationNote : Bool := { defValue := true }
 
 @[inherit_doc linter.adaptationNote]
 def adaptationNoteLinter : TextbasedLinter := fun opts lines ↦ Id.run do
@@ -213,7 +213,7 @@ def adaptationNoteLinter : TextbasedLinter := fun opts lines ↦ Id.run do
   return (errors, none)
 
 /-- Lint a collection of input strings if one of them contains trailing whitespace. -/
-register_option linter.trailingWhitespace : Bool := { defValue := true }
+public register_option linter.trailingWhitespace : Bool := { defValue := true }
 
 @[inherit_doc linter.trailingWhitespace]
 def trailingWhitespaceLinter : TextbasedLinter := fun opts lines ↦ Id.run do
@@ -229,7 +229,7 @@ def trailingWhitespaceLinter : TextbasedLinter := fun opts lines ↦ Id.run do
   return (errors, if errors.size > 0 then some fixedLines.toArray else none)
 
 /-- Lint a collection of input strings for a semicolon preceded by a space. -/
-register_option linter.whitespaceBeforeSemicolon : Bool := { defValue := true }
+public register_option linter.whitespaceBeforeSemicolon : Bool := { defValue := true }
 
 @[inherit_doc linter.whitespaceBeforeSemicolon]
 def semicolonLinter : TextbasedLinter := fun opts lines ↦ Id.run do
@@ -306,7 +306,7 @@ def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorC
 -- TODO: these linters assume they are being run in `./scripts` and do not work on
 -- downstream projects. Fix this before re-enabling them by default.
 -- Or better yet: port them to Lean 4.
-register_option linter.pythonStyle : Bool := { defValue := false }
+public register_option linter.pythonStyle : Bool := { defValue := false }
 
 /-- Lint a collection of modules for style violations.
 Print formatted errors for all unexpected style violations to standard output;
@@ -317,6 +317,7 @@ Return the number of files which had new style errors.
 `moduleNames` are the names of all the modules to lint,
 `mode` specifies what kind of output this script should produce,
 `fix` configures whether fixable errors should be corrected in-place. -/
+public
 def lintModules (opts : LinterOptions) (nolints : Array String) (moduleNames : Array Lean.Name)
     (style : ErrorFormat) (fix : Bool) : IO UInt32 := do
   let styleExceptions := parseStyleExceptions nolints
@@ -356,11 +357,12 @@ def lintModules (opts : LinterOptions) (nolints : Array String) (moduleNames : A
   return numberErrorFiles
 
 /-- Verify that all modules are named in `UpperCamelCase` -/
-register_option linter.modulesUpperCamelCase : Bool := { defValue := true }
+public register_option linter.modulesUpperCamelCase : Bool := { defValue := true }
 
 /-- Verifies that all modules in `modules` are named in `UpperCamelCase`
 (except for explicitly discussed exceptions, which are hard-coded here).
 Return the number of modules violating this. -/
+public -- only for MathlibTest/ModuleCase.lean
 def modulesNotUpperCamelCase (opts : LinterOptions) (modules : Array Lean.Name) : IO Nat := do
   unless getLinterValue linter.modulesUpperCamelCase opts do return 0
 
@@ -383,7 +385,7 @@ def modulesNotUpperCamelCase (opts : LinterOptions) (modules : Array Lean.Name)
   return badNames.size
 
 /-- Verify that no module name is forbidden according to Windows' filename rules. -/
-register_option linter.modulesForbiddenWindows : Bool := { defValue := true }
+public register_option linter.modulesForbiddenWindows : Bool := { defValue := true }
 
 /-- Verifies that no module in `modules` contains CON, PRN, AUX, NUL, COM1, COM2, COM3, COM4, COM5,
 COM6, COM7, COM8, COM9, COM¹, COM², COM³, LPT1, LPT2, LPT3, LPT4, LPT5, LPT6, LPT7, LPT8, LPT9,
@@ -394,6 +396,7 @@ Also verify that module names contain no forbidden characters such as `*`, `?` (
 
 Source: https://learn.microsoft.com/en-gb/windows/win32/fileio/naming-a-file.
 Return the number of module names violating this rule. -/
+public -- only for `MathlibTest/ForbiddenModuleNames`
 def modulesOSForbidden (opts : LinterOptions) (modules : Array Lean.Name) : IO Nat := do
   unless getLinterValue linter.modulesUpperCamelCase opts do return 0
   let forbiddenNames := [
diff --git a/Mathlib/Tactic/Linter/UnusedTactic.lean b/Mathlib/Tactic/Linter/UnusedTactic.lean
index ae59d6efe414e7..7a4dbba4a13c36 100644
--- a/Mathlib/Tactic/Linter/UnusedTactic.lean
+++ b/Mathlib/Tactic/Linter/UnusedTactic.lean
@@ -55,14 +55,14 @@ before and after and see if there is some change.
 Yet another linter copied from the `unreachableTactic` linter!
 -/
 
-public meta section
+meta section
 
 open Lean Elab Std Linter
 
 namespace Mathlib.Linter
 
 /-- The unused tactic linter makes sure that every tactic call actually changes *something*. -/
-register_option linter.unusedTactic : Bool := {
+public register_option linter.unusedTactic : Bool := {
   defValue := true
   descr := "enable the unused tactic linter"
 }
diff --git a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean
index 5f65fa6c8c3fb9..953f5880accd2e 100644
--- a/Mathlib/Tactic/Linter/UnusedTacticExtension.lean
+++ b/Mathlib/Tactic/Linter/UnusedTacticExtension.lean
@@ -15,7 +15,7 @@ This file defines the environment extension to keep track of which tactics are a
 the tactic state unchanged and not trigger the unused tactic linter.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command
 
@@ -25,7 +25,7 @@ namespace Mathlib.Linter.UnusedTactic
 Defines the `allowedUnusedTacticExt` extension for adding a `HashSet` of `allowedUnusedTactic`s
 to the environment.
 -/
-initialize allowedUnusedTacticExt :
+public initialize allowedUnusedTacticExt :
     SimplePersistentEnvExtension SyntaxNodeKind (Std.HashSet SyntaxNodeKind) ←
   registerSimplePersistentEnvExtension {
     addImportedFn := fun as => as.foldl Std.HashSet.insertMany {}
@@ -50,7 +50,7 @@ def addAllowedUnusedTactic {m : Type → Type} [Monad m] [MonadEnv m]
 /-- `Parser`s allowed to not change the tactic state.
 This can be increased dynamically, using `#allow_unused_tactic`.
 -/
-initialize allowedRef : IO.Ref (Std.HashSet SyntaxNodeKind) ←
+public initialize allowedRef : IO.Ref (Std.HashSet SyntaxNodeKind) ←
   IO.mkRef <| .ofArray #[
     `Mathlib.Tactic.Says.says,
     `Batteries.Tactic.«tacticOn_goal-_=>_»,
diff --git a/Mathlib/Tactic/Linter/UpstreamableDecl.lean b/Mathlib/Tactic/Linter/UpstreamableDecl.lean
index fd7bcfb881eb0e..d76d62c0e8ae4e 100644
--- a/Mathlib/Tactic/Linter/UpstreamableDecl.lean
+++ b/Mathlib/Tactic/Linter/UpstreamableDecl.lean
@@ -14,12 +14,13 @@ The `upstreamableDecl` linter detects declarations that could be moved to a file
 import hierarchy. This is intended to assist with splitting files.
 -/
 
-public meta section
+meta section
 
 open Lean Elab Command Linter
 
+-- TODO: move this to the `Lean` directory
 /-- Does this declaration come from the current file? -/
-def Lean.Name.isLocal (env : Environment) (decl : Name) : Bool :=
+public def Lean.Name.isLocal (env : Environment) (decl : Name) : Bool :=
   (env.getModuleIdxFor? decl).isNone
 
 open Mathlib.Command.MinImports
@@ -61,7 +62,7 @@ see options `linter.upstreamableDecl.defs` and `linter.upstreamableDecl.private`
 
 This is intended to assist with splitting files.
 -/
-register_option linter.upstreamableDecl : Bool := {
+public register_option linter.upstreamableDecl : Bool := {
   defValue := false
   descr := "enable the upstreamableDecl linter"
 }
@@ -73,7 +74,7 @@ The linter does not place a warning on any declaration depending on a definition
 (while it does place a warning on the definition itself), since we often create a new file for a
 definition on purpose.
 -/
-register_option linter.upstreamableDecl.defs : Bool := {
+public register_option linter.upstreamableDecl.defs : Bool := {
   defValue := false
   descr := "upstreamableDecl warns on definitions"
 }
@@ -81,7 +82,7 @@ register_option linter.upstreamableDecl.defs : Bool := {
 /--
 If set to `true`, the `upstreamableDecl` linter will add warnings on private declarations.
 -/
-register_option linter.upstreamableDecl.private : Bool := {
+public register_option linter.upstreamableDecl.private : Bool := {
   defValue := false
   descr := "upstreamableDecl warns on private declarations"
 }