dev: lint modules with just one exposed def, to manually inspect

Mathlib/CategoryTheory/MarkovCategory/Positive.lean

@@ -42,7 +42,7 @@ deterministic process.
 * [Moss and Perrone, *A category-theoretic proof of the ergodic decomposition theorem*][moss2023]
 -/
 
-@[expose] public section
+public section
 
 universe v u
 

Mathlib/Tactic/Linter/PrivateModule.lean

@@ -78,16 +78,29 @@ def privateModule : Linter where run stx := do
     if (← getEnv).header.isModule then
       -- Don't lint an imports-only module:
       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
+        let mut hasDef := false
+        let mut publicDefs := 0
+        let mut hasPublicItems := false
+        for (decl, val) in (← getEnv).constants.map₂ do
+          if val.isDefinition then
+            hasDef := true
+            -- Ignore both private and reserved names; see implementation notes
+            if !isPrivateName decl && !isReservedName (← getEnv) decl then
+              publicDefs := publicDefs + 1
+          else if !hasPublicItems then
+            if !isPrivateName decl && !isReservedName (← getEnv) decl then hasPublicItems := true
         -- 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`."
+        if !hasPublicItems then
+          logLint linter.privateModule topOfFileRef
+            s!"The current module only contains private declarations.\n\n\
+            Consider adding `{if hasDef then "@[expose] " else ""}public section` \
+            at the beginning of the module, or selectively marking declarations as `public`."
+        else if publicDefs == 1 then
+          -- TODO: check if we are in an expose'd section.
+          logLint linter.privateModule topOfFileRef
+            s!"The current module has exactly one public definition. \
+            Consider moving `@[expose]` there."
 
 initialize addLinter privateModule
 

MathlibTest/PrivateModuleLinter/hasOnlyPrivateNoDefs.lean

@@ -0,0 +1,28 @@
+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
+
+-- 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 `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