Deprecated attribute needs to be refined

[Zimmi48]

1. The deprecated attribute can be applied to any vernacular command, but it only has an effect on Ltac definitions. It is bad to not give an error message, or at least a warning, when it is applied on a command that is not supported.

2. Both the since= and note= sub-attributes are optional but you need to provide at least one of them. This doesn't make much sense. Note that providing note="" is not the same as not providing note because the printing won't be the same (more spaces in the former case). The same is true for since="" vs no since.

[maximedenes]

+1

[SkySkimmer]

TBH I'm not sure we want to have since, I would just have an optional note (which may include "since whenever" in the string).

[herbelin]

TBH I'm not sure we want to have since, I would just have an optional note (which may include "since whenever" in the string).

That makes sense, why not adopting this simplification.

Do we target 8.9 or 8.10? How to proceed?

[Zimmi48]

Do we target 8.9 or 8.10? How to proceed?

You target master for sure. You can put it in the 8.9.0 milestone if you want. Then the debate of whether it is backported or not can happen with the RM after the PR has been merged (or just before if this changes where to put the CHANGES entry).

[herbelin]

You target master for sure. You can put it in the 8.9.0 milestone if you want. Then the debate of whether it is backported or not can happen with the RM after the PR has been merged (or just before if this changes where to put the CHANGES entry).

Indeed, sounds reasonable.

I'm otherwise a bit lost in who wants to be involved. Should we make an "attributes" maintainer group?

Or maybe, the current de facto status, i.e. that attributes are under the supervision of @SkySkimmer is ok for anyone? Please anyone involved express his position.

[SkySkimmer]

The deprecated attribute can be applied to any vernacular command, but it only has an effect on Ltac definitions. It is bad to not give an error message, or at least a warning, when it is applied on a command that is not supported.

Should be solved now

Both the since= and note= sub-attributes are optional but you need to provide at least one of them. This doesn't make much sense. Note that providing note="" is not the same as not providing note because the printing won't be the same (more spaces in the former case). The same is true for since="" vs no since.

What do we want to do with this?

TBH I'm not sure we want to have since, I would just have an optional note (which may include "since whenever" in the string).

Now that we use since to categorize deprecation warnings we definitely want to keep it separate from the note.