From adef1f6b74d510a6e3172a0af22eb44b8229213a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 25 Apr 2026 09:46:09 +0200 Subject: [PATCH 1/5] fix(Linter/PrivateModule): only suggest @[expose] if the module has any definitions --- Mathlib/Tactic/Linter/PrivateModule.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean index 08905121646445..150a8ba0de32ee 100644 --- a/Mathlib/Tactic/Linter/PrivateModule.lean +++ b/Mathlib/Tactic/Linter/PrivateModule.lean @@ -78,6 +78,10 @@ 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 + let mut hasDef := false + for (decl, val) in (← getEnv).constants.map₂ do + if val.isDefinition then + hasDef := true -- 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 @@ -85,9 +89,9 @@ def privateModule : Linter where run stx := do -- 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`." + 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`." initialize addLinter privateModule From f7e66a0bfa1546ca4dbf46ff766cf075f37f925c Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 26 Apr 2026 09:50:59 +0200 Subject: [PATCH 2/5] Remove one more superfluous @[expose] --- Mathlib/CategoryTheory/MarkovCategory/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/MarkovCategory/Positive.lean b/Mathlib/CategoryTheory/MarkovCategory/Positive.lean index 3ea5eed004c795..4d3f0c8a13b106 100644 --- a/Mathlib/CategoryTheory/MarkovCategory/Positive.lean +++ b/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 From 0284a0377058af307d8c2e7e9823c9d0629ce68e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 27 Apr 2026 09:38:02 +0200 Subject: [PATCH 3/5] Fix typo; new test --- Mathlib/Tactic/Linter/PrivateModule.lean | 2 +- .../hasOnlyPrivateNoDefs.lean | 28 +++++++++++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 MathlibTest/PrivateModuleLinter/hasOnlyPrivateNoDefs.lean diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean index 150a8ba0de32ee..99593a76c6d060 100644 --- a/Mathlib/Tactic/Linter/PrivateModule.lean +++ b/Mathlib/Tactic/Linter/PrivateModule.lean @@ -90,7 +90,7 @@ def privateModule : Linter where run stx := do let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) "" logLint linter.privateModule topOfFileRef s!"The current module only contains private declarations.\n\n\ - Consider adding `{if hasDef then "`@[expose] " else ""}public section` \ + Consider adding `{if hasDef then "@[expose] " else ""}public section` \ at the beginning of the module, or selectively marking declarations as `public`." initialize addLinter privateModule diff --git a/MathlibTest/PrivateModuleLinter/hasOnlyPrivateNoDefs.lean b/MathlibTest/PrivateModuleLinter/hasOnlyPrivateNoDefs.lean new file mode 100644 index 00000000000000..6b7aadaa94eafa --- /dev/null +++ b/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 From 94ad049019f7f0839b27c4278575410f91021239 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 27 Apr 2026 09:41:25 +0200 Subject: [PATCH 4/5] wip: count all public defs --- Mathlib/Tactic/Linter/PrivateModule.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean index 99593a76c6d060..5a33028259147c 100644 --- a/Mathlib/Tactic/Linter/PrivateModule.lean +++ b/Mathlib/Tactic/Linter/PrivateModule.lean @@ -79,13 +79,16 @@ def privateModule : Linter where run stx := do -- Don't lint an imports-only module: if !(← getEnv).constants.map₂.isEmpty then 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 - -- 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 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 From c21dc5743538a01406df9bd368f6c179a682d387 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 27 Apr 2026 09:43:23 +0200 Subject: [PATCH 5/5] wip lint for exactly one item --- Mathlib/Tactic/Linter/PrivateModule.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Mathlib/Tactic/Linter/PrivateModule.lean b/Mathlib/Tactic/Linter/PrivateModule.lean index 5a33028259147c..291f1976038d57 100644 --- a/Mathlib/Tactic/Linter/PrivateModule.lean +++ b/Mathlib/Tactic/Linter/PrivateModule.lean @@ -91,10 +91,16 @@ def privateModule : Linter where run stx := do 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 - 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`." + 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