feat: missingDocs linter warns about empty doc strings

src/Lean/Elab/DocString.lean

@@ -85,6 +85,10 @@ structure State where
   -/
   lctx : LocalContext
   /--
+  The local instances.
+
+  The `MonadLift TermElabM DocM` instance runs the lifted action with these instances, so elaboration
+  commands that mutate this state cause it to take effect in subsequent commands.
   -/
   localInstances : LocalInstances
   /--

src/Lean/Linter/MissingDocs.lean

@@ -112,15 +112,37 @@ builtin_initialize
 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
   logLint linter.missingDocs stx m!"missing doc string for {msg}"
 
+def lintEmpty (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  logLint linter.missingDocs stx m!"empty doc string for {msg}"
+
 def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {stx.getId}"
 
+def lintEmptyNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lintEmpty stx s!"{msg} {stx.getId}"
+
 def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+def lintEmptyField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lintEmpty stx s!"{msg} {parent.getId}.{stx.getId}"
+
 def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+private def isEmptyDocString (docOpt : Syntax) : CommandElabM Bool := do
+  if docOpt.isNone then return false
+  let docStx : TSyntax `Lean.Parser.Command.docComment := ⟨docOpt[0]⟩
+  -- Verso doc comments with interpolated content cannot be extracted as plain text,
+  -- but they are clearly not empty.
+  if let .node _ `Lean.Parser.Command.versoCommentBody _ := docStx.raw[1] then
+    if !docStx.raw[1][0].isAtom then return false
+  let text ← getDocStringText docStx
+  return text.trimAscii.isEmpty
+
+def isMissingDoc (docOpt : Syntax) : CommandElabM Bool := do
+  return docOpt.isNone || (← isEmptyDocString docOpt)
+
 def hasInheritDoc (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.simple &&
@@ -130,38 +152,68 @@ def hasTacticAlt (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.tactic_alt
 
-def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
+def declModifiersDocStatus (mods : Syntax) : CommandElabM (Option Bool) := do
   let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
     mods[2][0].getKind == ``Command.public else
     mods[2][0].getKind != ``Command.private
-  return isPublic && mods[0].isNone && !hasInheritDoc mods[1]
+  if !isPublic || hasInheritDoc mods[1] then return none
+  if mods[0].isNone then return some false
+  if (← isEmptyDocString mods[0]) then return some true
+  return none
 
-def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
-  if k == ``«abbrev» then lintNamed id "public abbrev"
-  else if k == ``definition then lintNamed id "public def"
-  else if k == ``«opaque» then lintNamed id "public opaque"
-  else if k == ``«axiom» then lintNamed id "public axiom"
-  else if k == ``«inductive» then lintNamed id "public inductive"
-  else if k == ``classInductive then lintNamed id "public inductive"
-  else if k == ``«structure» then lintNamed id "public structure"
+def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
+  return (← declModifiersDocStatus mods).isSome
+
+private def lintDocStatus (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  if isEmpty then lintEmpty stx msg else lint stx msg
+
+private def lintDocStatusNamed (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
+  if isEmpty then lintEmptyNamed stx msg else lintNamed stx msg
+
+private def lintDocStatusField (isEmpty : Bool) (parent stx : Syntax) (msg : String) :
+    CommandElabM Unit :=
+  if isEmpty then lintEmptyField parent stx msg else lintField parent stx msg
+
+def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) (isEmpty : Bool := false) :
+    CommandElabM Unit := do
+  if k == ``«abbrev» then lintDocStatusNamed isEmpty id "public abbrev"
+  else if k == ``definition then lintDocStatusNamed isEmpty id "public def"
+  else if k == ``«opaque» then lintDocStatusNamed isEmpty id "public opaque"
+  else if k == ``«axiom» then lintDocStatusNamed isEmpty id "public axiom"
+  else if k == ``«inductive» then lintDocStatusNamed isEmpty id "public inductive"
+  else if k == ``classInductive then lintDocStatusNamed isEmpty id "public inductive"
+  else if k == ``«structure» then lintDocStatusNamed isEmpty id "public structure"
+
+private def docOptStatus (docOpt attrs : Syntax) (checkTacticAlt := false) :
+    CommandElabM (Option Bool) := do
+  if hasInheritDoc attrs then return none
+  if checkTacticAlt && hasTacticAlt attrs then return none
+  if docOpt.isNone then return some false
+  if (← isEmptyDocString docOpt) then return some true
+  return none
 
 @[builtin_missing_docs_handler declaration]
 def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``Command.private then return -- not private
   let k := rest.getKind
-  if (← declModifiersPubNoDoc head) then -- no doc string
-    lintDeclHead k rest[1][0]
+  if let some isEmpty ← declModifiersDocStatus head then
+    lintDeclHead k rest[1][0] isEmpty
   if k == ``«inductive» || k == ``classInductive then
     for stx in rest[4].getArgs do
       let head := stx[2]
-      if stx[0].isNone && (← declModifiersPubNoDoc head) then
-        lintField rest[1][0] stx[3] "public constructor"
+      -- Constructor has two doc comment positions: the leading one before `|` (stx[0])
+      -- and the one inside declModifiers (head[0]). If either is non-empty, skip.
+      let leadingEmpty ← isEmptyDocString stx[0]
+      if !stx[0].isNone && !leadingEmpty then
+        pure () -- constructor has a non-empty leading doc comment
+      else if let some modsEmpty ← declModifiersDocStatus head then
+        lintDocStatusField (leadingEmpty || modsEmpty) rest[1][0] stx[3] "public constructor"
     unless rest[5].isNone do
       for stx in rest[5][0][1].getArgs do
         let head := stx[0]
-        if (← declModifiersPubNoDoc head) then -- no doc string
-          lintField rest[1][0] stx[1] "computed field"
+        if let some isEmpty ← declModifiersDocStatus head then
+          lintDocStatusField isEmpty rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
     unless rest[4][2].isNone do
       let redecls : Std.HashSet String.Pos.Raw :=
@@ -173,45 +225,52 @@ def checkDecl : SimpleHandler := fun stx => do
               else s
             else s
       let parent := rest[1][0]
-      let lint1 stx := do
+      let lint1 isEmpty stx := do
         if let some range := stx.getRange? then
           if redecls.contains range.start then return
-        lintField parent stx "public field"
+        lintDocStatusField isEmpty parent stx "public field"
       for stx in rest[4][2][0].getArgs do
         let head := stx[0]
-        if (← declModifiersPubNoDoc head) then
+        if let some isEmpty ← declModifiersDocStatus head then
           if stx.getKind == ``structSimpleBinder then
-            lint1 stx[1]
+            lint1 isEmpty stx[1]
           else
             for stx in stx[2].getArgs do
-              lint1 stx
+              lint1 isEmpty stx
 
 @[builtin_missing_docs_handler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
-  if !stx[2].isNone && (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[2][0] "initializer"
+  if !stx[2].isNone then
+    if let some isEmpty ← declModifiersDocStatus stx[0] then
+      lintDocStatusNamed isEmpty stx[2][0] "initializer"
 
 @[builtin_missing_docs_handler «notation»]
 def checkNotation : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
-    if stx[5].isNone then lint stx[3] "notation"
-    else lintNamed stx[5][0][3] "notation"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "notation"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "notation"
 
 @[builtin_missing_docs_handler «mixfix»]
 def checkMixfix : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
-    if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal
-    else lintNamed stx[5][0][3] stx[3][0].getAtomVal
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] stx[3][0].getAtomVal
+      else lintDocStatusNamed isEmpty stx[5][0][3] stx[3][0].getAtomVal
 
 @[builtin_missing_docs_handler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "syntax"
-    else lintNamed stx[5][0][3] "syntax"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "syntax"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "syntax"
 
 def mkSimpleHandler (name : String) (declNameStxIdx := 2) : SimpleHandler := fun stx => do
-  if stx[0].isNone then
-    lintNamed stx[declNameStxIdx] name
+  if (← isMissingDoc stx[0]) then
+    if (← isEmptyDocString stx[0]) then
+      lintEmptyNamed stx[declNameStxIdx] name
+    else
+      lintNamed stx[declNameStxIdx] name
 
 @[builtin_missing_docs_handler syntaxAbbrev]
 def checkSyntaxAbbrev : SimpleHandler := mkSimpleHandler "syntax"
@@ -221,20 +280,22 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtin_missing_docs_handler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "macro"
-    else lintNamed stx[5][0][3] "macro"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "macro"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "macro"
 
 @[builtin_missing_docs_handler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
-    if stx[5].isNone then lint stx[3] "elab"
-    else lintNamed stx[5][0][3] "elab"
+  if stx[2][0][0].getKind != ``«local» then
+    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
+      if stx[5].isNone then lintDocStatus isEmpty stx[3] "elab"
+      else lintDocStatusNamed isEmpty stx[5][0][3] "elab"
 
 @[builtin_missing_docs_handler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
-  if (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[3] "class abbrev"
+  if let some isEmpty ← declModifiersDocStatus stx[0] then
+    lintDocStatusNamed isEmpty stx[3] "class abbrev"
 
 @[builtin_missing_docs_handler Parser.Tactic.declareSimpLikeTactic]
 def checkSimpLike : SimpleHandler := mkSimpleHandler "simp-like tactic"
@@ -244,8 +305,8 @@ def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler (declNameStxId
 
 @[builtin_missing_docs_handler Option.registerOption]
 def checkRegisterOption : SimpleHandler := fun stx => do
-  if (← declModifiersPubNoDoc stx[0]) then
-    lintNamed stx[2] "option"
+  if let some isEmpty ← declModifiersDocStatus stx[0] then
+    lintDocStatusNamed isEmpty stx[2] "option"
 
 @[builtin_missing_docs_handler registerSimpAttr]
 def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"

tests/elab/linterCoe.lean

@@ -27,7 +27,7 @@ Note: This linter can be disabled with `set_option linter.deprecatedCoercions fa
 #guard_msgs in
 def h (foo : X) : Y := foo
 
-/-- -/
+/-- A docstring to make `missingDocs` linter happy-/
 notation a " +' " b => a + b
 
 @[deprecated "" (since := "")]

tests/elab/linterMissingDocs.lean

@@ -105,3 +105,37 @@ def handleMyCmd : SimpleHandler := fun
 my_command y
 
 my_command z
+
+-- Test: empty doc strings should be treated as missing
+/---/
+def emptyDoc1 (x : Nat) := x
+
+/--
+-/
+def emptyDoc2 (x : Nat) := x
+
+/--   -/
+def emptyDoc3 (x : Nat) := x
+
+-- Test: empty doc strings on other declaration kinds
+/---/
+inductive EmptyInd where
+  /---/ | emptyCtorDoc
+  | noCtorDoc
+
+/---/
+notation:20 "empty_nota" x y => Nat.add x y
+
+/---/
+macro "empty_macro" : term => `(my_elab)
+
+/---/
+elab "empty_elab" : term => return Lean.mkConst ``false
+
+-- Test: @[inherit_doc] suppresses even with empty doc
+@[inherit_doc hasDoc]
+def inheritedDoc (x : Nat) := x
+
+-- Test: Verso doc comments with interpolated content are not empty
+/-- See {name}`hasDoc` for details. -/
+def versoDoc (x : Nat) := x

tests/elab/linterMissingDocs.lean.out.expected

@@ -109,3 +109,30 @@ Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:107:11-107:12: warning: missing doc string for my_command z
 
 Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:111:4-111:13: warning: empty doc string for public def emptyDoc1
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:115:4-115:13: warning: empty doc string for public def emptyDoc2
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:118:4-118:13: warning: empty doc string for public def emptyDoc3
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:122:10-122:18: warning: empty doc string for public inductive EmptyInd
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:123:10-123:22: warning: empty doc string for public constructor EmptyInd.emptyCtorDoc
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:124:4-124:13: warning: missing doc string for public constructor EmptyInd.noCtorDoc
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:127:0-127:8: warning: empty doc string for notation
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:130:0-130:5: warning: empty doc string for macro
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:133:0-133:4: warning: empty doc string for elab
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`