Deprecating `str` syntax for docstrings in `to_additive`

Stream: mathlib4

[Thomas Murrills]

#28135 will (eventually) deprecate str syntax support for additive docstrings, e.g. @[to_additive "I am an additive docstring!"], in favor of docComment syntax, e.g. @[to_additive /-- I am an additive docstring! -/]. Note that it will not remove support for str syntax, but instead will issue a warning and provide a suggestion.

There are two questions I'd like to ask in this thread:

1. Who should str syntax be deprecated for? As I see it, there are three options: (a.) everyone in mathlib (b.) everyone adhering to mathlib style standards through linter options (c.) everyone
2. When should support for str be removed, and seeing as the deprecation is not a declaration deprecation, how should this be recorded?

[Eric Wieser]

I would say the answer to 1 is (c)

[Eric Wieser]

Ideally with a "try this" to make adapting downstream easier

[Thomas Murrills]

Eric Wieser said:

I would say the answer to 1 is (c)

Okay—hmm, in that case, I suppose the next question is whether this warning should be (i.) controlled by linter.deprecated (ii.) controlled by a new option (iii.) not controlled by an option.

[Thomas Murrills]

Eric Wieser said:

Ideally with a "try this" to make adapting downstream easier

Yup—by "provide a suggestion", I meant "provide a Suggestion"! :)

[Eric Wieser]

I think emulating the standard deprecation machinery as much as possible is the right thing to do here

[Eric Wieser]

So respect the options, phrase the warning message in the same way, and log with the same tag on the message

[Eric Wieser]

Arguably core (and in the meantime, mathlib) should have a helper function for that

[Thomas Murrills]

True; I may as well PR that helper function to mathlib first.

[Violeta Hernández]

Out of curiosity, what's the benefit of this?

[Aaron Liu]

less escaping

[Aaron Liu]

more clear it's a docstring since it uses the docstring syntax

[Aaron Liu]

gives you better syntax highlighting

[Violeta Hernández]

Valid

[Thomas Murrills]

Eric Wieser said:

So respect the options, phrase the warning message in the same way, and log with the same tag on the message

Aside: minor point, but I think the phrasing of current deprecation warning code actions should say "Update to: <new>" instead of "Replace <old> with <new>" to (1.) better communicate the fact that this is coming from a deprecation (2.) keep code actions concise. (Also, code formatting is not rendered in code action titles, and so I believe we should avoid backticks if possible. Separation-by-colon is enough, imo.)

[Thomas Murrills]

Also, I'm wondering: do we think the suggestion widget text should duplicate the logged message as much as possible, or not?

The argument to the contrary would be that they both appear in the infoview, so duplicating them is noisy; we can instead separate their roles, and have the message be descriptive of the general issue, while the suggestion is only descriptive of the specific change necessary. E.g. the widget could simply say "Update deprecated syntax to:\n<clickable new version>", while the logged message could say "<This kind> of syntax is deprecated: use <this kind> of syntax instead". (If the specific change necessary is large, this could be a more comprehensible description of the issue in a log.)

[Thomas Murrills]

Are there contexts where it is useful to have the intended replacement in the logged message per se? For example, are interactive suggestions available in the neovim extension?