max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: account for tactic_alt in missing docs linter (#10507)

Browse source 
This PR makes the missing docs linter aware of `tactic_alt`.
This commit is contained in:
Sebastian Graf 2025-09-22 18:23:24 +02:00 • committed by GitHub
parent 2b23afdfab
commit 795d13ddce
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 23 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Linter/MissingDocs.lean
View file

@ -126,6 +126,10 @@ def hasInheritDoc (attrs : Syntax) : Bool :=
attr[1].isOfKind ``Parser.Attr.simple &&
attr[1][0].getId.eraseMacroScopes == `inherit_doc
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
let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
mods[2][0].getKind == ``Command.public else
@ -201,7 +205,7 @@ def checkMixfix : SimpleHandler := fun stx => do
@[builtin_missing_docs_handler «syntax»]
def checkSyntax : SimpleHandler := fun stx => do
if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
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"
@ -217,13 +221,13 @@ 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] then
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"
@[builtin_missing_docs_handler «elab»]
def checkElab : SimpleHandler := fun stx => do
if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
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"

16
tests/lean/run/missingDocsTacticAlt.lean Normal file
View file

@ -0,0 +1,16 @@
module
public import Lean
set_option linter.missingDocs true
/-- Docstring -/
syntax (name := test) "test" : tactic
@[tactic_alt test]
syntax "test1" : tactic
@[tactic_alt test]
macro "test2" : tactic => `(tactic| test1)
@[tactic_alt test]
elab "test2" : tactic => return ()