Verso docstring syntax error messages do not suggest correct fixes

[Vierkantor]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When a Verso declaration docstring uses contains a syntax error, the parser error tends to be unclear and suggested fixes do not resolve the parse error.

set_option doc.verso true

/--
{module =checked}`Mathlib`
-/ -- two errors appear at this line:
-- error: '}'
-- unexpected end of input; expected '![', '$$', '$', '[' or '[^'
def foo := 37

-- Follow the suggestion:
/--
{module =checked}`Mathlib`
![-/ -- two errors appear at this line:
-- error: '}'
-- unexpected end of input; expected '![', '$$', '$', '[' or '[^'
def foo' := 37

-- Follow another suggestion:
/--
{module =checked}`Mathlib`
$-/ -- two errors appear at this line:
-- error: '}'
-- unexpected end of input; expected '![', '$$', '$', '[' or '[^'
def foo'' := 37



/--
[`rigid` --> `flexible`]
-/ -- one error appears at the end of the previous line:
-- error: expected '(' or '['
def bar := 37

-- Follow the suggestion:
/--
[`rigid` --> `flexible`[]
-/ -- one error appears at the end of the previous line:
-- error: expected ']'
def bar' := 37

-- Follow the suggestion again:
/--
[`rigid` --> `flexible`[]]
-/ -- one error appears at the end of the previous line:
-- error: expected ']'
def bar'' := 37

-- Et cetera

This makes it hard to debug issues with Verso docstrings.

Context

I encountered this when experimenting with enabling Verso docstrings for Mathlib: a lot of Mathlib's docstrings are incompatible with Verso, so having good error messages is important for the fix.

Steps to Reproduce

1. Write a declaration docstring with a syntax error.

Expected behavior: An error message describing the precise syntax error in a way that the fix is easy to find.

Actual behavior: An error message that suggests corrections that do not help.

Versions

Lean 4.27.0-rc1 (Mathlib, MacOS / Darwin Kernel Version 23.6.0 / arm64), Lean 4.28.0-nightly-2026-01-19 (Lean4web nightly)

Additional Information

See also issue #12062 for unhelpful error messages in a module docstring context.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.