feat: MissingDocs doesn't lint on struct redecl

src/Lean/Elab/InfoTree/Main.lean

@@ -152,6 +152,9 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
   f!"FVarAlias {info.id.name} -> {info.baseId.name}"
 
+def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
+  f!"FieldRedecl @ {formatStxRange ctx info.stx}"
+
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
@@ -159,9 +162,10 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofMacroExpansionInfo i => i.format ctx
   | ofFieldInfo i          => i.format ctx
   | ofCompletionInfo i     => i.format ctx
-  | ofUserWidgetInfo i     => pure <| UserWidgetInfo.format i
+  | ofUserWidgetInfo i     => pure <| i.format
   | ofCustomInfo i         => pure <| Std.ToFormat.format i
-  | ofFVarAliasInfo i      => pure <| FVarAliasInfo.format i
+  | ofFVarAliasInfo i      => pure <| i.format
+  | ofFieldRedeclInfo i    => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
@@ -173,6 +177,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofUserWidgetInfo _     => none
   | ofCustomInfo _         => none
   | ofFVarAliasInfo _      => none
+  | ofFieldRedeclInfo _    => none
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.

src/Lean/Elab/InfoTree/Types.lean

@@ -102,6 +102,18 @@ structure FVarAliasInfo where
   id     : FVarId
   baseId : FVarId
 
+/--
+Contains the syntax of an identifier which is part of a field redeclaration, like:
+```
+structure Foo := x : Nat
+structure Bar extends Foo :=
+  x := 0
+--^ here
+```
+-/
+structure FieldRedeclInfo where
+  stx : Syntax
+
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
@@ -113,6 +125,7 @@ inductive Info where
   | ofUserWidgetInfo (i : UserWidgetInfo)
   | ofCustomInfo (i : CustomInfo)
   | ofFVarAliasInfo (i : FVarAliasInfo)
+  | ofFieldRedeclInfo (i : FieldRedeclInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/Elab/Structure.lean

@@ -557,6 +557,7 @@ where
                 valStx ← `(fun $(view.binders.getArgs)* => $valStx:term)
               let fvarType ← inferType info.fvar
               let value ← Term.elabTermEnsuringType valStx fvarType
+              pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref }
               let infos := updateFieldInfoVal infos info.name value
               go (i+1) defaultValsOverridden infos
         match info.kind with

src/Lean/Linter/MissingDocs.lean

@@ -107,6 +107,9 @@ def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
 def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
+  lint stx s!"{msg} {parent.getId}.{stx.getId}"
+
 def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
   if k == ``«abbrev» then lintNamed id "public abbrev"
   else if k == ``«def» then lintNamed id "public def"
@@ -136,14 +139,27 @@ def checkDecl : SimpleHandler := fun stx => do
           lintField rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
     unless rest[5].isNone || rest[5][2].isNone do
+      let redecls : Std.HashSet String.Pos :=
+        (← get).infoState.trees.foldl (init := {}) fun s tree =>
+          tree.foldInfo (init := s) fun _ info s =>
+            if let .ofFieldRedeclInfo info := info then
+              if let some range := info.stx.getRange? then
+                s.insert range.start
+              else s
+            else s
+      let parent := rest[1][0]
+      let lint1 stx := do
+        if let some range := stx.getRange? then
+          if redecls.contains range.start then return
+        lintField parent stx "public field"
       for stx in rest[5][2][0].getArgs do
         let head := stx[0]
         if head[2][0].getKind != ``«private» && head[0].isNone then
           if stx.getKind == ``structSimpleBinder then
-            lintField rest[1][0] stx[1] "public field"
+            lint1 stx[1]
           else
             for stx in stx[2].getArgs do
-              lintField rest[1][0] stx "public field"
+              lint1 stx
 
 @[builtinMissingDocsHandler «initialize»]
 def checkInit : SimpleHandler := fun stx => do

src/Lean/Server/InfoUtils.lean

@@ -22,7 +22,7 @@ def Lean.Syntax.getRange? (stx : Syntax) (originalOnly := false) : Option String
 namespace Lean.Elab
 
 /-- Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up. -/
-partial def InfoTree.visitM [Monad m] [Inhabited α]
+partial def InfoTree.visitM [Monad m]
     (preNode  : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
     (postNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → List (Option α) → m α)
     : InfoTree → m (Option α) :=
@@ -95,6 +95,7 @@ def Info.stx : Info → Syntax
   | ofCustomInfo i         => i.stx
   | ofUserWidgetInfo i     => i.stx
   | ofFVarAliasInfo _      => .missing
+  | ofFieldRedeclInfo i    => i.stx
 
 def Info.lctx : Info → LocalContext
   | Info.ofTermInfo i  => i.lctx

tests/lean/linterMissingDocs.lean

@@ -54,10 +54,18 @@ structure Foo where
   [mk6 mk7 : Nat]
 
 class Bar (α : Prop) := mk ::
+  (foo bar := 1)
+
+class Bar2 (α : Prop) where
+  bar := 2
+
+class Bar3 (α : Prop) extends Bar α where
+  bar := 3
+  (foo baz := 3)
 
 theorem aThm : True := trivial
 example : True := trivial
-instance : Bar True := ⟨⟩
+instance : Bar True := {}
 
 initialize init : Unit ← return
 initialize return

tests/lean/linterMissingDocs.lean.expected.out

@@ -14,14 +14,20 @@ linterMissingDocs.lean:53:7-53:10: warning: missing doc string for public field
 linterMissingDocs.lean:54:3-54:6: warning: missing doc string for public field Foo.mk6 [linter.missingDocs]
 linterMissingDocs.lean:54:7-54:10: warning: missing doc string for public field Foo.mk7 [linter.missingDocs]
 linterMissingDocs.lean:56:6-56:9: warning: missing doc string for public structure Bar [linter.missingDocs]
-linterMissingDocs.lean:62:11-62:15: warning: missing doc string for initializer init [linter.missingDocs]
-linterMissingDocs.lean:65:19-65:24: warning: missing doc string for syntax category myCat [linter.missingDocs]
-linterMissingDocs.lean:67:0-67:6: warning: missing doc string for syntax [linter.missingDocs]
-linterMissingDocs.lean:68:16-68:24: warning: missing doc string for syntax namedSyn [linter.missingDocs]
-linterMissingDocs.lean:75:0-75:4: warning: missing doc string for elab [linter.missingDocs]
-linterMissingDocs.lean:76:0-76:5: warning: missing doc string for macro [linter.missingDocs]
-linterMissingDocs.lean:78:13-78:22: warning: missing doc string for class abbrev [anonymous] [linter.missingDocs]
-linterMissingDocs.lean:80:16-80:24: warning: missing doc string for option myOption [linter.missingDocs]
-linterMissingDocs.lean:82:14-82:19: warning: missing doc string for elab myCmd [linter.missingDocs]
-linterMissingDocs.lean:88:4-88:15: warning: missing doc string for public def handleMyCmd [linter.missingDocs]
-linterMissingDocs.lean:95:11-95:12: warning: missing doc string for my_command z [linter.missingDocs]
+linterMissingDocs.lean:57:3-57:6: warning: missing doc string for public field Bar.foo [linter.missingDocs]
+linterMissingDocs.lean:57:7-57:10: warning: missing doc string for public field Bar.bar [linter.missingDocs]
+linterMissingDocs.lean:59:6-59:10: warning: missing doc string for public structure Bar2 [linter.missingDocs]
+linterMissingDocs.lean:60:2-60:5: warning: missing doc string for public field Bar2.bar [linter.missingDocs]
+linterMissingDocs.lean:62:6-62:10: warning: missing doc string for public structure Bar3 [linter.missingDocs]
+linterMissingDocs.lean:64:7-64:10: warning: missing doc string for public field Bar3.baz [linter.missingDocs]
+linterMissingDocs.lean:70:11-70:15: warning: missing doc string for initializer init [linter.missingDocs]
+linterMissingDocs.lean:73:19-73:24: warning: missing doc string for syntax category myCat [linter.missingDocs]
+linterMissingDocs.lean:75:0-75:6: warning: missing doc string for syntax [linter.missingDocs]
+linterMissingDocs.lean:76:16-76:24: warning: missing doc string for syntax namedSyn [linter.missingDocs]
+linterMissingDocs.lean:83:0-83:4: warning: missing doc string for elab [linter.missingDocs]
+linterMissingDocs.lean:84:0-84:5: warning: missing doc string for macro [linter.missingDocs]
+linterMissingDocs.lean:86:13-86:22: warning: missing doc string for class abbrev [anonymous] [linter.missingDocs]
+linterMissingDocs.lean:88:16-88:24: warning: missing doc string for option myOption [linter.missingDocs]
+linterMissingDocs.lean:90:14-90:19: warning: missing doc string for elab myCmd [linter.missingDocs]
+linterMissingDocs.lean:96:4-96:15: warning: missing doc string for public def handleMyCmd [linter.missingDocs]
+linterMissingDocs.lean:103:11-103:12: warning: missing doc string for my_command z [linter.missingDocs]