feat: add @[inheritDoc] attribute

src/Lean/Elab.lean

@@ -43,3 +43,4 @@ import Lean.Elab.BuiltinCommand
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.Eval
 import Lean.Elab.Calc
+import Lean.Elab.InheritDoc

src/Lean/Elab/InheritDoc.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.InfoTree.Main
+import Lean.DocString
+
+namespace Lean
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name := `inheritDoc
+    descr := "inherit documentation from a specified declaration"
+    add   := fun decl stx kind => do
+      unless kind == AttributeKind.global do
+        throwError "invalid `[inheritDoc]` attribute, must be global"
+      match stx with
+      | `(attr| inheritDoc $[$id?:ident]?) =>
+        let some id := id?
+          | throwError "invalid `[inheritDoc]` attribute, could not infer doc source"
+        let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id
+        if (← findDocString? (← getEnv) decl).isSome then
+          logWarningAt id m!"{← mkConstWithLevelParams decl} already has a doc string"
+        let some doc ← findDocString? (← getEnv) declName
+          | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
+        addDocString decl doc
+      | _  => throwError "invalid `[inheritDoc]` attribute"
+  }

src/Lean/Elab/Notation.lean

@@ -24,6 +24,18 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
     | Syntax.node i k args => Syntax.node i k (args.map (antiquote vars))
     | stx => stx
 
+ def addInheritDocDefault (rhs : Term) (attrs? : Option (TSepArray ``attrInstance ",")) :
+    Option (TSepArray ``attrInstance ",") :=
+  attrs?.map fun attrs =>
+    match rhs with
+    | `($f:ident $_args*) =>
+      attrs.getElems.map fun stx => Unhygienic.run do
+        if let `(attrInstance| $attr:ident) := stx then
+          if attr.getId.eraseMacroScopes == `inheritDoc then
+            return ← `(attrInstance| $attr:ident $f:ident)
+        pure ⟨stx⟩
+    | _ => attrs
+
 /-- Convert `notation` command lhs item into a `syntax` command item -/
 def expandNotationItemIntoSyntaxItem : TSyntax ``notationItem → MacroM (TSyntax `stx)
   | `(notationItem| $_:ident$[:$prec?]?) => `(stx| term $[:$prec?]?)
@@ -124,6 +136,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
   let vars := items.filter fun item => item.raw.getKind == ``identPrec
   let vars := vars.map fun var => var.raw[0]
   let qrhs := ⟨antiquote vars rhs⟩
+  let attrs? := addInheritDocDefault rhs attrs?
   let patArgs ← items.mapM expandNotationItemIntoPattern
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/

src/Lean/Linter/MissingDocs.lean

@@ -110,6 +110,14 @@ def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
 def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+def hasInheritDoc (attrs : Syntax) : Bool :=
+  attrs[0][1].getSepArgs.any fun attr =>
+    attr[1].isOfKind ``Parser.Attr.simple &&
+    attr[1][0].getId.eraseMacroScopes == `inheritDoc
+
+def declModifiersPubNoDoc (mods : Syntax) : Bool :=
+  mods[2][0].getKind != ``«private» && mods[0].isNone && !hasInheritDoc mods[1]
+
 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"
@@ -124,21 +132,20 @@ def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``«private» then return -- not private
   let k := rest.getKind
-  if head[0].isNone then -- no doc string
+  if declModifiersPubNoDoc head then -- no doc string
     lintDeclHead k rest[1][0]
   if k == ``«inductive» || k == ``classInductive then
     for stx in rest[4].getArgs do
       let head := stx[1]
-      if head[2][0].getKind != ``«private» && head[0].isNone then
+      if declModifiersPubNoDoc head then
         lintField rest[1][0] stx[2] "public constructor"
     unless rest[5].isNone do
       for stx in rest[5][0][1].getArgs do
         let head := stx[0]
-        if head[2][0].getKind == ``«private» then return -- not private
-        if head[0].isNone then -- no doc string
+        if declModifiersPubNoDoc head then -- no doc string
           lintField rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
-    unless rest[5].isNone || rest[5][2].isNone do
+    unless 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 =>
@@ -154,7 +161,7 @@ def checkDecl : SimpleHandler := fun stx => do
         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 declModifiersPubNoDoc head then
           if stx.getKind == ``structSimpleBinder then
             lint1 stx[1]
           else
@@ -163,25 +170,24 @@ def checkDecl : SimpleHandler := fun stx => do
 
 @[builtinMissingDocsHandler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
-  if stx[2].isNone then return
-  if stx[0][2][0].getKind != ``«private» && stx[0][0].isNone then
+  if !stx[2].isNone && declModifiersPubNoDoc stx[0] then
     lintNamed stx[2][0] "initializer"
 
 @[builtinMissingDocsHandler «notation»]
 def checkNotation : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  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"
 
 @[builtinMissingDocsHandler «mixfix»]
 def checkMixfix : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  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!
 
 @[builtinMissingDocsHandler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1]  then
     if stx[5].isNone then lint stx[3] "syntax"
     else lintNamed stx[5][0][3] "syntax"
 
@@ -209,8 +215,7 @@ def checkElab : SimpleHandler := fun stx => do
 
 @[builtinMissingDocsHandler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
-  let head := stx[0]
-  if head[2][0].getKind != ``«private» && head[0].isNone then
+  if declModifiersPubNoDoc stx[0] then
     lintNamed stx[3] "class abbrev"
 
 @[builtinMissingDocsHandler Parser.Tactic.declareSimpLikeTactic]

tests/lean/interactive/hover.lean

@@ -69,8 +69,8 @@ elab_rules : term
 #check mynota' 1
      --^ textDocument/hover
 
-infix:65 " >+< " => Nat.add
-                   --^ textDocument/hover
+@[inheritDoc] infix:65 " >+< " => Nat.add
+                                 --^ textDocument/hover
 
 #check 1 >+< 2
         --^ textDocument/hover