From f395593ffce1b94cdd025ba51c23aa5eeef7e353 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 30 Mar 2026 20:48:25 +0100 Subject: [PATCH] feat: `missingDocs` linter warns about empty doc strings (#13188) This PR extends the `missingDocs` linter to detect and warn about empty doc strings (e.g. `/---/` or `/-- -/`), in addition to missing doc strings. Previously, an empty doc comment would silence the linter even though it provides no documentation value. Now empty doc strings produce a distinct "empty doc string for ..." warning, while `@[inherit_doc]` still suppresses warnings as before. --- src/Lean/Elab/DocString.lean | 4 + src/Lean/Linter/MissingDocs.lean | 149 ++++++++++++------ tests/elab/linterCoe.lean | 2 +- tests/elab/linterMissingDocs.lean | 34 ++++ .../elab/linterMissingDocs.lean.out.expected | 27 ++++ 5 files changed, 171 insertions(+), 45 deletions(-) diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean index 8b30dfa3b3..71054c3e47 100644 --- a/src/Lean/Elab/DocString.lean +++ b/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 /-- diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 0ec1a78dea..8f69209259 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/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" diff --git a/tests/elab/linterCoe.lean b/tests/elab/linterCoe.lean index ff87634bc2..dc538d3320 100644 --- a/tests/elab/linterCoe.lean +++ b/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 := "")] diff --git a/tests/elab/linterMissingDocs.lean b/tests/elab/linterMissingDocs.lean index 4dc41177bd..76547a6d6e 100644 --- a/tests/elab/linterMissingDocs.lean +++ b/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 diff --git a/tests/elab/linterMissingDocs.lean.out.expected b/tests/elab/linterMissingDocs.lean.out.expected index 8cd20dc078..1d5617ff81 100644 --- a/tests/elab/linterMissingDocs.lean.out.expected +++ b/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`