Commit 2025-08-12 21:40 8df47aec

feat: deprecate str syntax for to_additive docstrings in Mathlib (#28135) This PR deprecates str syntax for to_additive docstrings in favor of docComment syntax: @[to_additive /-- I am an additive docstring! -/] instead of @[to_additive "I am an additive docstring!"]. It does so by adding a warning and an interactive suggestion/code action to replace the str syntax with the corresponding docComment syntax. It also reformats docstrings which have appeared since writing #28066. This deprecation attempts to hew closely to the standard deprecation trappings, but makes two idiosyncratic choices:

• Since docstrings are usually verbose, we split the role of the interactive suggestion from the role of the logged message. The logged message describes the cause of the error (in general), while trying to emulate the standard phrasing:

  String syntax for to_additive docstrings is deprecated: Use docstring syntax instead (e.g. @[to_additive /-- example -/])

  while the interactive suggestion only suggests the replacement:

  Update deprecated syntax to: /-- <clickable new docstring here> -/

• Likewise, to keep the code action as concise and communicative as possible, instead of saying "Replace `<old>` with `<new>`", we say "Update to: <new>". (We also don't include backticks, since they are not rendered in code action titles and the colon is sufficient separation.) See also this zulip thread.