feat: privateModule linter (#31820)

This linter lints against nonempty modules that have only private declarations, and suggests adding `@[expose] public section` to the top.

This linter found 1 violation in Mathlib, which was fixed in #31822.

Co-authored-by: thorimur <thomasmurrills@gmail.com>
Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>
Co-authored-by: Bryan Gin-ge Chen <5209952+bryangingechen@users.noreply.github.com>

Author: 3 people

Mathlib.lean

@@ -6450,6 +6450,7 @@ public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PPRoundtrip
+public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
 public import Mathlib.Tactic.Linter.TextBased
 public import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/Init.lean

@@ -16,6 +16,7 @@ public import Mathlib.Tactic.Linter.FlexibleLinter
 public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
+public import Mathlib.Tactic.Linter.PrivateModule
 -- The following import contains the environment extension for the unused tactic linter.
 public import Mathlib.Tactic.Linter.UnusedTacticExtension
 public import Mathlib.Tactic.Linter.UnusedTactic
@@ -67,6 +68,7 @@ register_linter_set linter.mathlibStandardSet :=
   -- linter.checkInitImports -- disabled, not relevant downstream.
   linter.hashCommand
   linter.oldObtain
+  linter.privateModule
   linter.style.cases
   linter.style.induction
   linter.style.refine

Mathlib/Tactic.lean

@@ -171,6 +171,7 @@ public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PPRoundtrip
+public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
 public import Mathlib.Tactic.Linter.TextBased
 public import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/Tactic/Linter.lean

@@ -13,4 +13,5 @@ public meta import Mathlib.Tactic.Linter.DeprecatedModule
 public meta import Mathlib.Tactic.Linter.HaveLetLinter
 public meta import Mathlib.Tactic.Linter.MinImports
 public meta import Mathlib.Tactic.Linter.PPRoundtrip
+public meta import Mathlib.Tactic.Linter.PrivateModule
 public meta import Mathlib.Tactic.Linter.UpstreamableDecl

Mathlib/Tactic/Linter/PrivateModule.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2025 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+public meta import Lean.Elab.Command
+public import Lean.Linter.Basic
+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
+
+/-!
+# Private module linter
+
+This linter lints against nonempty modules that have only private declarations, and suggests adding
+`@[expose] public section` to the top or selectively marking declarations as `public`.
+
+## Implementation notes
+
+`env.constants.map₂` contains all locally-defined constants, and accessing this waits until all
+declarations are added. By linting (only) the `eoi` token, we can capture all constants defined in
+the file.
+
+Note that private declarations are exactly those which satisfy `isPrivateName`, whether private due
+to an explicit `private` or due to not being made `public`.
+-/
+
+meta section
+
+open Lean Elab Command Linter
+
+namespace Mathlib.Linter
+
+/-- The `privateModule` linter lints against nonempty modules that have only private declarations,
+and suggests adding `@[expose] public section` or selectively marking declarations as `public`. -/
+public register_option linter.privateModule : Bool := {
+  defValue := false
+  descr := "Enable the `privateModule` linter, which lints against nonempty modules that have only \
+    private declarations."
+}
+
+/--
+The `privateModule` linter lints against nonempty modules that have only private declarations,
+and suggests adding `@[expose] public section` to the top.
+
+This linter only acts on the end-of-input `Parser.Command.eoi` token, and ignores all other syntax.
+It logs its message at the top of the file.
+-/
+def privateModule : Linter where run stx := do
+  if stx.isOfKind ``Parser.Command.eoi then
+    unless getLinterValue linter.privateModule (← getLinterOptions) do
+      return
+    if (← getEnv).header.isModule then
+      -- Don't lint an imports-only module:
+      if !(← getEnv).constants.map₂.isEmpty then
+        -- Exit if any declaration is public:
+        for (decl, _) in (← getEnv).constants.map₂ do
+          if !isPrivateName decl then return
+        -- Lint if all names are private:
+        let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
+        logLint linter.privateModule topOfFileRef
+          "The current module only contains private declarations.\n\n\
+          Consider adding `@[expose] public section` at the beginning of the module, \
+          or selectively marking declarations as `public`."
+
+initialize addLinter privateModule
+
+end Mathlib.Linter

MathlibTest/PrivateModuleLinter/hasOnlyPrivate.lean

@@ -0,0 +1,30 @@
+module
+
+import Mathlib.Init
+import all Mathlib.Tactic.Linter.PrivateModule
+import Lean.Elab.Command
+
+open Lean
+
+set_option linter.mathlibStandardSet true
+
+theorem foo : True := trivial
+
+def bar : Bool := true
+
+-- Run the linter on artificial `eoi` syntax so that we can actually guard the message
+open Mathlib.Linter Parser in
+/--
+warning: The current module only contains private declarations.
+
+Consider adding `@[expose] public section` at the beginning of the module, or selectively marking declarations as `public`.
+
+Note: This linter can be disabled with `set_option linter.privateModule false`
+-/
+#guard_msgs in
+run_cmd do
+  let eoi := mkNode ``Command.eoi #[mkAtom .none ""]
+  privateModule.run eoi
+
+-- Disable so that this test is silent
+set_option linter.privateModule false

MathlibTest/PrivateModuleLinter/hasPublic.lean

@@ -0,0 +1,9 @@
+module
+
+import Mathlib.Tactic.Linter.PrivateModule
+
+set_option linter.privateModule true
+
+-- Should not fire, since `foo` is `public`.
+
+public theorem foo : True := trivial

MathlibTest/PrivateModuleLinter/importOnly.lean

@@ -0,0 +1,8 @@
+module
+
+import Mathlib.Tactic.Linter.PrivateModule
+import Mathlib.Logic.Basic
+
+set_option linter.privateModule true
+
+/- Should not fire, since the file has no declarations. -/

MathlibTest/PrivateModuleLinter/nonModule.lean

@@ -0,0 +1,9 @@
+import Mathlib.Tactic.Linter.PrivateModule
+
+set_option linter.privateModule true
+
+/- Should not fire because this file does not use `module`, even though it is nonempty and has only private defs. -/
+
+private theorem foo : True := trivial
+
+private def bar : Bool := true