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.
This commit is contained in:
Wojciech Różowski
GitHub
parent
a88f81bc28
commit
f395593ffc
5 changed files with 171 additions and 45 deletions
|
|
@ -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
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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 := "")]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue