fix: report Verso docsring parse errors (#12314)

This PR fixes a problem where Verso docstring parse errors were being
swallowed in some circumstances.

Closes #12062.

src/Lean/DocString/Add.lean

@@ -98,6 +98,51 @@ def parseVersoDocString
 
 
 
+open Lean.Parser Command in
+/--
+Reports parse errors from a Verso docstring parse failure.
+
+When Verso docstring parsing fails at parse time, a `parseFailure` node is created containing the
+raw text, because emitting an error at that stage could lead to unwanted parser backtracking. This
+function reports the actual error messages with proper source positions.
+-/
+def reportVersoParseFailure
+    [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
+    [MonadResolveName m]
+    (parseFailure : Syntax) : m Unit := do
+  let some rawAtom := parseFailure[0]?
+    | return  -- malformed node, nothing to report
+  let some startPos := rawAtom.getPos? (canonicalOnly := true)
+    | return
+  let some endPos := rawAtom.getTailPos? (canonicalOnly := true)
+    | return
+
+  let text ← getFileMap
+  let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos
+  have endPos_valid : endPos ≤ text.source.rawEndPos := by
+    unfold endPos; split <;> simp [*]
+
+  let env ← getEnv
+  let ictx : InputContext :=
+    .mk text.source (← getFileName) (fileMap := text)
+      (endPos := endPos) (endPos_valid := endPos_valid)
+  let pmctx : ParserModuleContext := {
+    env,
+    options := ← getOptions,
+    currNamespace := ← getCurrNamespace,
+    openDecls := ← getOpenDecls
+  }
+  let s := mkParserState text.source |>.setPos startPos
+  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
+
+  for (pos, _, err) in s.allErrors do
+    logMessage {
+      fileName := ← getFileName,
+      pos := text.toPosition pos,
+      data := err.toString,
+      severity := .error
+    }
+
 open Lean.Doc in
 open Lean.Parser.Command in
 /--

src/Lean/Elab/BuiltinCommand.lean

@@ -27,8 +27,13 @@ namespace Lean.Elab.Command
     else
       throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present."
   | Syntax.node _ ``Lean.Parser.Command.versoCommentBody args =>
-    runTermElabM fun _ => do
-      addVersoModDocString range ⟨args.getD 0 .missing⟩
+    let docSyntax := args.getD 0 .missing
+    if docSyntax.getKind == `Lean.Doc.Syntax.parseFailure then
+      -- Report parser errors without attempting elaboration
+      runTermElabM fun _ => reportVersoParseFailure docSyntax
+    else
+      runTermElabM fun _ => do
+        addVersoModDocString range ⟨docSyntax⟩
   | _ => throwErrorAt stx "unexpected module doc string{indentD <| stx}"
 
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name)

tests/lean/run/versoDocParseError.lean

@@ -0,0 +1,45 @@
+import Lean
+
+set_option doc.verso true
+
+/-!
+This test ensures that syntax errors in Verso docs are appropriately reported.
+-/
+
+-- Syntax error in module docstring should report actual error location
+/--
+error: '}'
+---
+error: unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+-/
+#guard_msgs in
+/-!
+Here is text with an unclosed role {name`Nat
+-/
+
+-- Syntax error with specific position (not at end of docstring)
+/--
+@ +2:27...*
+error: '*'
+-/
+#guard_msgs (positions := true) in
+/-!
+Some mismatched *formatting_
+
+A b c d e f.
+
+```
+-/
+
+-- Syntax error in a normal docstring
+/--
+@ +2:27...*
+error: '*'
+-/
+#guard_msgs (positions := true) in
+/--
+Some mismatched *formatting_
+
+A b c d e f.
+-/
+def x := 5