deprecated annotation

Stream: std4

[James Gallicchio]

We've talked about it before, but any thoughts on adding a @[deprecated] annotation with linter support to warn at the use site (probably with text that describes the new name to use?)? Thinking about it cuz of std4#177, which includes breaking changes for mathlib that would be easy to fix downstream if there were nice linter messages saying what the new names are.

[Kyle Miller]

Have you tried using @[deprecated foo]? It seems to do everything you're suggesting, except perhaps linting.

[Ruben Van de Velde]

We have this in mathlib; I thought it came from core or std already

[Kyle Miller]

Yeah, it's in core

[James Gallicchio]

oh very cool

[James Gallicchio]

I would prefer if it allowed strings instead of just (known) identifiers... Maybe I try to find the core implementation.

[Kyle Miller]

I'm not sure how that would work -- you need to have a declaration around with the old name so that you can resolve the name downstream to be able to give the warning.

[James Gallicchio]

The warning can just include the string instead of the "use whatever instead" message

[James Gallicchio]

vscode displays the warning nicely so I don't think any additional linter is necessary :)

[James Gallicchio]

oh, @Kyle Miller I meant having something like @[deprecated "See patch notes"] def foo, for when there is no new symbol to substitute for the deprecated one