feat: @[builtin_doc] attribute (part 2) (#3918)

This solves the issue where certain subexpressions are lacking syntax
hovers because the hover text is not "builtin" - it only shows up if the
`Parser` constant is imported in the environment. For top level syntaxes
this is not a problem because `builtin_term_parser` will automatically
add this doc information, but nested syntaxes don't get the same
treatment.

We could walk the expression and add builtin docs recursively, but this
is somewhat expensive and unnecessary given that it's a fixed list of
declarations in lean core. Moreover, there are reasons to want to
control which syntax nodes actually get hovers, and while a better
system for that is forthcoming, for now it can be achieved by
strategically not applying the `@[builtin_doc]` attribute.

Fixes #3842

src/Lean/Elab/InheritDoc.lean

@@ -21,7 +21,7 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findSimpleDocString? (← getEnv) decl).isSome then
+        if (← findSimpleDocString? (← getEnv) decl (includeBuiltin := false)).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
         let some doc ← findSimpleDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"

src/Lean/Parser/Basic.lean

@@ -145,7 +145,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
 /-- Generate an error at the position saved with the `withPosition` combinator.
    If `delta == true`, then it reports at saved position+1.
    This useful to make sure a parser consumed at least one character.  -/
-def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
+@[builtin_doc] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
   fn := errorAtSavedPosFn msg delta
 }
 
@@ -271,7 +271,7 @@ def orelseFn (p q : ParserFn) : ParserFn :=
   NOTE: In order for the pretty printer to retrace an `orelse`, `p` must be a call to `node` or some other parser
   producing a single node kind. Nested `orelse` calls are flattened for this, i.e. `(node k1 p1 <|> node k2 p2) <|> ...`
   is fine as well. -/
-def orelse (p q : Parser) : Parser where
+@[builtin_doc] def orelse (p q : Parser) : Parser where
   info := orelseInfo p.info q.info
   fn   := orelseFn p.fn q.fn
 
@@ -295,7 +295,7 @@ This is important for the `p <|> q` combinator, because it is not backtracking,
 `p` fails after consuming some tokens. To get backtracking behavior, use `atomic(p) <|> q` instead.
 
 This parser has the same arity as `p` - it produces the same result as `p`. -/
-def atomic : Parser → Parser := withFn atomicFn
+@[builtin_doc] def atomic : Parser → Parser := withFn atomicFn
 
 /-- Information about the state of the parse prior to the failing parser's execution -/
 structure RecoveryContext where
@@ -335,7 +335,7 @@ state immediately after the failure.
 
 The interactions between <|> and `recover'` are subtle, especially for syntactic
 categories that admit user extension. Consider avoiding it in these cases. -/
-def recover' (parser : Parser) (handler : RecoveryContext → Parser) : Parser where
+@[builtin_doc] def recover' (parser : Parser) (handler : RecoveryContext → Parser) : Parser where
   info := parser.info
   fn := recoverFn parser.fn fun s => handler s |>.fn
 
@@ -347,7 +347,7 @@ If `handler` fails itself, then no recovery is performed.
 
 The interactions between <|> and `recover` are subtle, especially for syntactic
 categories that admit user extension. Consider avoiding it in these cases. -/
-def recover (parser handler : Parser) : Parser := recover' parser fun _ => handler
+@[builtin_doc] def recover (parser handler : Parser) : Parser := recover' parser fun _ => handler
 
 def optionalFn (p : ParserFn) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
@@ -378,7 +378,7 @@ position to the original state on success. So for example `lookahead("=>")` will
 next token is `"=>"`, without actually consuming this token.
 
 This parser has arity 0 - it does not capture anything. -/
-def lookahead : Parser → Parser := withFn lookaheadFn
+@[builtin_doc] def lookahead : Parser → Parser := withFn lookaheadFn
 
 def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
@@ -394,7 +394,7 @@ def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
 if `p` succeeds then it fails with the message `"unexpected foo"`.
 
 This parser has arity 0 - it does not capture anything. -/
-def notFollowedBy (p : Parser) (msg : String) : Parser where
+@[builtin_doc] def notFollowedBy (p : Parser) (msg : String) : Parser where
   fn := notFollowedByFn p.fn msg
 
 partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run do
@@ -1143,7 +1143,7 @@ def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
 For example, the parser `"foo" ws "+"` parses `foo +` or `foo/- -/+` but not `foo+`.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkWsBefore (errorMsg : String := "space before") : Parser where
+@[builtin_doc] def checkWsBefore (errorMsg : String := "space before") : Parser where
   info := epsilonInfo
   fn   := checkWsBeforeFn errorMsg
 
@@ -1160,7 +1160,7 @@ def checkLinebreakBeforeFn (errorMsg : String) : ParserFn := fun _ s =>
 (The line break may be inside a comment.)
 
 This parser has arity 0 - it does not capture anything. -/
-def checkLinebreakBefore (errorMsg : String := "line break") : Parser where
+@[builtin_doc] def checkLinebreakBefore (errorMsg : String := "line break") : Parser where
   info := epsilonInfo
   fn   := checkLinebreakBeforeFn errorMsg
 
@@ -1180,7 +1180,7 @@ This is almost the same as `"foo+"`, but using this parser will make `foo+` a to
 problems for the use of `"foo"` and `"+"` as separate tokens in other parsers.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
+@[builtin_doc] def checkNoWsBefore (errorMsg : String := "no space before") : Parser := {
   info := epsilonInfo
   fn   := checkNoWsBeforeFn errorMsg
 }
@@ -1430,7 +1430,7 @@ position (see `withPosition`). This can be used to do whitespace sensitive synta
 a `by` block or `do` block, where all the lines have to line up.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkColEq (errorMsg : String := "checkColEq") : Parser where
+@[builtin_doc] def checkColEq (errorMsg : String := "checkColEq") : Parser where
   fn := checkColEqFn errorMsg
 
 def checkColGeFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1449,7 +1449,7 @@ certain indentation scope. For example it is used in the lean grammar for `else
 that the `else` is not less indented than the `if` it matches with.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkColGe (errorMsg : String := "checkColGe") : Parser where
+@[builtin_doc] def checkColGe (errorMsg : String := "checkColGe") : Parser where
   fn := checkColGeFn errorMsg
 
 def checkColGtFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1473,7 +1473,7 @@ Here, the `revert` tactic is followed by a list of `colGt ident`, because otherw
 interpret `exact` as an identifier and try to revert a variable named `exact`.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkColGt (errorMsg : String := "checkColGt") : Parser where
+@[builtin_doc] def checkColGt (errorMsg : String := "checkColGt") : Parser where
   fn := checkColGtFn errorMsg
 
 def checkLineEqFn (errorMsg : String) : ParserFn := fun c s =>
@@ -1491,7 +1491,7 @@ different lines. For example, `else if` is parsed using `lineEq` to ensure that
 are on the same line.
 
 This parser has arity 0 - it does not capture anything. -/
-def checkLineEq (errorMsg : String := "checkLineEq") : Parser where
+@[builtin_doc] def checkLineEq (errorMsg : String := "checkLineEq") : Parser where
   fn := checkLineEqFn errorMsg
 
 /-- `withPosition(p)` runs `p` while setting the "saved position" to the current position.
@@ -1507,7 +1507,7 @@ The saved position is only available in the read-only state, which is why this i
 after the `withPosition(..)` block the saved position will be restored to its original value.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withPosition : Parser → Parser := withFn fun f c s =>
+@[builtin_doc] def withPosition : Parser → Parser := withFn fun f c s =>
     adaptCacheableContextFn ({ · with savedPos? := s.pos }) f c s
 
 def withPositionAfterLinebreak : Parser → Parser := withFn fun f c s =>
@@ -1519,7 +1519,7 @@ parsers like `colGt` will have no effect. This is usually used by bracketing con
 `(...)` so that the user can locally override whitespace sensitivity.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withoutPosition (p : Parser) : Parser :=
+@[builtin_doc] def withoutPosition (p : Parser) : Parser :=
   adaptCacheableContext ({ · with savedPos? := none }) p
 
 /-- `withForbidden tk p` runs `p` with `tk` as a "forbidden token". This means that if the token
@@ -1529,15 +1529,15 @@ stop there, making `tk` effectively a lowest-precedence operator. This is used f
 would be treated as an application.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withForbidden (tk : Token) (p : Parser) : Parser :=
+@[builtin_doc] def withForbidden (tk : Token) (p : Parser) : Parser :=
   adaptCacheableContext ({ · with forbiddenTk? := tk }) p
 
 /-- `withoutForbidden(p)` runs `p` disabling the "forbidden token" (see `withForbidden`), if any.
 This is usually used by bracketing constructs like `(...)` because there is no parsing ambiguity
 inside these nested constructs.
 
 This parser has the same arity as `p` - it just forwards the results of `p`. -/
-def withoutForbidden (p : Parser) : Parser :=
+@[builtin_doc] def withoutForbidden (p : Parser) : Parser :=
   adaptCacheableContext ({ · with forbiddenTk? := none }) p
 
 def eoiFn : ParserFn := fun c s =>
@@ -1692,7 +1692,7 @@ def termParser (prec : Nat := 0) : Parser :=
 -- ==================
 
 /-- Fail if previous token is immediately followed by ':'. -/
-def checkNoImmediateColon : Parser := {
+@[builtin_doc] def checkNoImmediateColon : Parser := {
   fn := fun c s =>
     let prev := s.stxStack.back
     if checkTailNoWs prev then
@@ -1756,7 +1756,7 @@ def unicodeSymbol (sym asciiSym : String) : Parser :=
   Define parser for `$e` (if `anonymous == true`) and `$e:name`.
   `kind` is embedded in the antiquotation's kind, and checked at syntax `match` unless `isPseudoKind` is true.
   Antiquotations can be escaped as in `$$e`, which produces the syntax tree for `$e`. -/
-def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser :=
+@[builtin_doc] def mkAntiquot (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parser :=
   let kind := kind ++ (if isPseudoKind then `pseudo else .anonymous) ++ `antiquot
   let nameP := node `antiquotName <| checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name
   -- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
@@ -1781,7 +1781,7 @@ def withAntiquotFn (antiquotP p : ParserFn) (isCatAntiquot := false) : ParserFn
     p c s
 
 /-- Optimized version of `mkAntiquot ... <|> p`. -/
-def withAntiquot (antiquotP p : Parser) : Parser := {
+@[builtin_doc] def withAntiquot (antiquotP p : Parser) : Parser := {
   fn := withAntiquotFn antiquotP.fn p.fn
   info := orelseInfo antiquotP.info p.info
 }
@@ -1791,7 +1791,7 @@ def withoutInfo (p : Parser) : Parser := {
 }
 
 /-- Parse `$[p]suffix`, e.g. `$[p],*`. -/
-def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
+@[builtin_doc] def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
   let kind := kind ++ `antiquot_scope
   leadingNode kind maxPrec <| atomic <|
     setExpected [] "$" >>
@@ -1808,7 +1808,7 @@ private def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (suffix : ParserF
   s.mkNode (kind ++ `antiquot_suffix_splice) (s.stxStack.size - 2)
 
 /-- Parse `suffix` after an antiquotation, e.g. `$x,*`, and put both into a new node. -/
-def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
+@[builtin_doc] def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
   info := andthenInfo p.info suffix.info
   fn c s :=
     let s := p.fn c s

src/Lean/Parser/Command.lean

@@ -78,21 +78,24 @@ All modifiers are optional, and have to come in the listed order.
 `nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
 on the same line as the declaration. It is used for declarations nested inside other syntax,
 such as inductive constructors, structure projections, and `let rec` / `where` definitions. -/
-def declModifiers (inline : Bool) := leading_parser
+@[builtin_doc] def declModifiers (inline : Bool) := leading_parser
   optional docComment >>
   optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >>
   optional visibility >>
   optional «noncomputable» >>
   optional «unsafe» >>
   optional («partial» <|> «nonrec»)
 /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/
-def declId           := leading_parser
+-- @[builtin_doc] -- FIXME: suppress the hover
+def declId := leading_parser
   ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}")
 /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/
-def declSig          := leading_parser
+-- @[builtin_doc] -- FIXME: suppress the hover
+def declSig := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
 /-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/
-def optDeclSig       := leading_parser
+-- @[builtin_doc] -- FIXME: suppress the hover
+def optDeclSig := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
 /-- Right-hand side of a `:=` in a declaration, a term. -/
 def declBody : Parser :=
@@ -141,11 +144,11 @@ def whereStructInst  := leading_parser
 * a sequence of `| pat => expr` (a declaration by equations), shorthand for a `match`
 * `where` and then a sequence of `field := value` initializers, shorthand for a structure constructor
 -/
-def declVal          :=
+@[builtin_doc] def declVal :=
   -- Remark: we should not use `Term.whereDecls` at `declVal`
   -- because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes.
   -- Issue #753 shows an example that fails to be parsed when we used `Term.whereDecls`.
-  withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
+  withAntiquot (mkAntiquot "declVal" decl_name% (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
 def «abbrev»         := leading_parser
   "abbrev " >> declId >> ppIndent optDeclSig >> declVal
@@ -193,9 +196,10 @@ inductive List (α : Type u) where
 ```
 A list of elements of type `α` is either the empty list, `nil`,
 or an element `head : α` followed by a list `tail : List α`.
-For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).
+See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
+for more information.
 -/
-def «inductive»      := leading_parser
+@[builtin_doc] def «inductive» := leading_parser
   "inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
   many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
 def classInductive   := leading_parser
@@ -544,7 +548,7 @@ def openSimple       := leading_parser
 def openScoped       := leading_parser
   " scoped" >> many1 (ppSpace >> checkColGt >> ident)
 /-- `openDecl` is the body of an `open` declaration (see `open`) -/
-def openDecl         :=
+@[builtin_doc] def openDecl :=
   withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <|
     openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
 /-- Makes names from other namespaces visible without writing the namespace prefix.

src/Lean/Parser/Do.lean

@@ -30,7 +30,7 @@ def doSeqBracketed := leading_parser
 do elements that take blocks. It can either have the form `"{" (doElem ";"?)* "}"` or
 `many1Indent (doElem ";"?)`, where `many1Indent` ensures that all the items are at
 the same or higher indentation level as the first line. -/
-def doSeq          :=
+@[builtin_doc] def doSeq :=
   withAntiquot (mkAntiquot "doSeq" decl_name% (isPseudoKind := true)) <|
     doSeqBracketed <|> doSeqIndent
 /-- `termBeforeDo` is defined as `withForbidden("do", term)`, which will parse a term but