From d96fd949ffb7aa9fa0e4ee0f152327578d1f1855 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Tue, 23 Sep 2025 18:18:21 +0200
Subject: [PATCH] fix: invalid docstring suggestions for attributes (#10522)

This also exposed an issue with `#guard_msgs` in Verso mode where the
docstring would log parse errors as if it contained Verso, even though
it actually worked. This has been fixed, and error messages improved as
well.
---
 src/Lean/DocString/Add.lean          |  2 +-
 src/Lean/Elab/DocString/Builtin.lean | 10 ++++--
 src/Lean/Parser/Term.lean            | 26 +++++++++++---
 tests/lean/run/versoDocs.lean        | 53 +++++++++++++++++++++++++---
 4 files changed, 78 insertions(+), 13 deletions(-)

diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean
index 40f1fb9a6b..554b0a19da 100644
--- a/src/Lean/DocString/Add.lean
+++ b/src/Lean/DocString/Add.lean
@@ -159,7 +159,7 @@ def versoDocStringFromString
   }
   let s := mkParserState docComment
   -- TODO parse one block at a time for error recovery purposes
-  let s := (Doc.Parser.document).run ictx pmctx (getTokenTable env) s
+  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
 
   if !s.allErrors.isEmpty then
     for (pos, _, err) in s.allErrors do
diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean
index ab1bfa6a16..4614b4db55 100644
--- a/src/Lean/Elab/DocString/Builtin.lean
+++ b/src/Lean/Elab/DocString/Builtin.lean
@@ -976,8 +976,14 @@ def suggestAttr (code : StrLit) : DocM (Array CodeSuggestion) := do
   catch
     | _ => pure ()
   try
-    discard <| parseStrLit attrParser.fn code
-    return #[.mk ``attr none none]
+    let stx ← parseStrLit attrParser.fn code
+    if stx.getKind == ``Lean.Parser.Attr.simple then
+      let attrName := stx[0].getId.eraseMacroScopes
+      if isAttribute (← getEnv) attrName then
+        return #[.mk ``attr none none]
+      else return #[]
+    else
+      return #[.mk ``attr none none]
   catch
     | _ => pure ()
   return #[]
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 8d55a787d8..d8ba1baf1d 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -28,19 +28,35 @@ def versoCommentBodyFn : ParserFn := fun c s =>
   let startPos := s.pos
   let s := finishCommentBlock (pushMissingOnError := true) 1 c s
   if !s.hasError then
+    let iniSz := s.stackSize
     let commentEndPos := s.pos
     let endPos := c.prev (c.prev commentEndPos)
     let endPos := if endPos ≤ c.inputString.endPos then endPos else c.inputString.endPos
     let c' := c.setEndPos endPos (by unfold endPos; split <;> simp [*])
     let s := Doc.Parser.document {} c' (s.setPos startPos)
-    if s.hasError then
-      s.pushSyntax .missing
-    else
-      (rawFn (Doc.Parser.ignoreFn <| chFn '-' >> chFn '/') (trailingWs := true)) c s
+    let s :=
+      if !s.allErrors.isEmpty then
+        -- Docstring parsing must always succeed, or else later error messages are atrocious! Syntax
+        -- errors in the docs should not cause verso-docstring-expecting commands to be removed from
+        -- consideration. So, at this stage, we push an indication of the failure, and then later,
+        -- when adding docstrings, the failing case is re-parsed and the errors are reported then.
+        -- We don't just parse them later because then the syntax of the docs doesn't end up as part
+        -- of the syntax of the actual program.
+        let s := s.restore iniSz endPos
+        let leading := c.mkEmptySubstringAt startPos
+        let trailing := c.mkEmptySubstringAt endPos
+        let s :=
+          s.pushSyntax <|
+          .atom (.original leading startPos trailing endPos) (c.inputString.extract startPos endPos)
+        let s := s.mkNode `Lean.Doc.Syntax.parseFailure iniSz
+        {s with recoveredErrors := #[]}
+      else s
+    rawFn (Doc.Parser.ignoreFn <| chFn '-' >> chFn '/') (trailingWs := true) c s
   else s
 
 public def versoCommentBody : Parser where
-  fn := nodeFn `Lean.Parser.Command.versoCommentBody versoCommentBodyFn
+  fn := fun c s => nodeFn `Lean.Parser.Command.versoCommentBody versoCommentBodyFn c s
+
 
 @[combinator_parenthesizer versoCommentBody, expose]
 public def versoCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean
index 9e795c413b..9779b4e3c7 100644
--- a/tests/lean/run/versoDocs.lean
+++ b/tests/lean/run/versoDocs.lean
@@ -9,11 +9,6 @@ This test checks that the basic features of Verso docstrings work.
 open Lean Doc Elab Term
 
 
-
-
-
-
-
 @[doc_code_block]
 def c (s : StrLit) : DocM (Block ElabInline ElabBlock) := pure (Block.code (s.getString.toList.reverse |> String.mk))
 
@@ -365,6 +360,54 @@ def yetMore' := ()
 
 #check yetMore'
 
+-- Test that only actual attributes lead to suggestions
+/--
+warning: Code element could be more specific.
+
+Hint: Insert a role to document it:
+  • {̲a̲t̲t̲r̲}̲`instance`
+  • {̲k̲w̲ ̲(̲o̲f̲ ̲:̲=̲ ̲L̲e̲a̲n̲.̲P̲a̲r̲s̲e̲r̲.̲A̲t̲t̲r̲.̲i̲n̲s̲t̲a̲n̲c̲e̲)̲}̲`instance` (in `attr`)
+  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`instance`
+---
+warning: Code element could be more specific.
+
+Hint: Insert a role to document it:
+  • {̲a̲t̲t̲r̲}̲`term_elab`
+  • {̲g̲i̲v̲e̲n̲}̲`term_elab`
+  • {̲l̲e̲a̲n̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲f̲i̲n̲e̲P̲a̲t̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲v̲e̲r̲t̲P̲a̲t̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`term_elab`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`term_elab`
+---
+warning: Code element could be more specific.
+
+Hint: Insert a role to document it:
+  • {̲g̲i̲v̲e̲n̲}̲`instantiation`
+  • {̲l̲e̲a̲n̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲f̲i̲n̲e̲P̲a̲t̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲v̲e̲r̲t̲P̲a̲t̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`instantiation`
+  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`instantiation`
+-/
+#guard_msgs in
+/--
+This one has its own parser: `instance`
+This one is an identifier: `term_elab`
+This is not an attribute: `instantiation`
+-/
+def attrSuggestionTest := ()
+
 /-
 TODO test:
 * Scope rules for all operators