chore: ignore autoparam declarations in private module linter

Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

@@ -19,6 +19,8 @@ functions for `p < ∞`.
 This result is recorded in `MeasureTheory.MemLp.exist_sub_eLpNorm_le`.
 -/
 
+@[expose] public section
+
 variable {α β E F : Type*} [MeasurableSpace E] [NormedAddCommGroup F]
 
 open scoped Nat NNReal ContDiff

Mathlib/Tactic/Linter/PrivateModule.lean

@@ -45,9 +45,15 @@ declarations, the linter should still fire on `M.Bar`. Ignoring reserved names e
 See also the type `Lean.ReservedNameAction`, invocations of `registerReservedNameAction` and
 `registerReservedNamePredicate` for examples, and the module `Lean.ResolveName` for further insight.
 
+We also do not count declarations which begin with `_auto`, as these are always-public auxiliary
+declarations created to hold the syntax of autoparams. It is not clear yet whether they are
+intended to be public, but for now we avoid them.
+See lean4#11569 and [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/PrivateModule.20linter.20not.20firing/near/562418477).
+
 Note that metaprograms should not add public declarations when run in private scopes. Doing so would
 likely be a bug in the metaprogram. As such, we do not perform further checks for automatically
-generated declarations such as those in `isAutoDecl`.
+generated declarations such as those detected by `isAutoDecl` or `isInternalDetail`, which would
+wrongly exclude e.g. public declarations generated by `initialize`.
 -/
 
 meta section
@@ -80,8 +86,11 @@ def privateModule : Linter where run stx := do
       if !(← getEnv).constants.map₂.isEmpty then
         -- Exit if any declaration from the current module is public:
         for (decl, _) in (← getEnv).constants.map₂ do
-          -- Ignore both private and reserved names; see implementation notes
-          if !isPrivateName decl && !isReservedName (← getEnv) decl then return
+          -- Ignore private, reserved, and autoparam names; see implementation notes
+          if !isPrivateName decl
+              && !isReservedName (← getEnv) decl
+              && !(`_auto).isPrefixOf decl then
+            return
         -- Lint if all names are private:
         let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
         logLint linter.privateModule topOfFileRef

MathlibTest/PrivateModuleLinter/initialize.lean

@@ -0,0 +1,17 @@
+module
+
+import Mathlib.Tactic.Linter.PrivateModule
+
+set_option linter.privateModule true
+
+open Lean
+
+-- Should not fire, since `initialize` creates a genuinely public declaration.
+initialize pure ()
+
+/- Check that we have indeed created a declaration, and aren't not linting just due to being an
+empty file: -/
+/-- info: [initFn✝] -/
+#guard_msgs in
+run_cmd do
+  logInfo m!"{(← getEnv).constants.map₂.toArray.map (MessageData.ofConstName ·.1)}"