Premature deprecations in 8.16rc1

[xavierleroy]

I like my CompCert development to compile cleanly without stdlib deprecation warnings in at least 3 consecutive versions of Coq.

This has been possible for quite a while now, but 8.16rc1 breaks this property:

• Ropp_inv_permute is deprecated in 8.16 but its recommended replacement, Rinv_opp, was introduced in 8.16 too. So, Ropp_inv_permute should not be deprecated until 8.19.
• Z_div_mod_eq is deprecated in 8.16 but its recommended replacement, Z_div_mod_eq_full, changed type between 8.13 and 8.14 (an hypothesis b <> 0 was removed), making it essentially unusable in a development that should build both before and after 8.14. So, Z_div_mod_eq should not be deprecated until 8.17.

Thank you in advance for putting a little more discipline and thoughts into stdlib deprecation warnings.

[xavierleroy]

Cc @proux01 @silene .

[SkySkimmer]

Z_div_mod_eq is deprecated in 8.16 but its recommended replacement, Z_div_mod_eq_full, changed type between 8.13 and 8.14 (an hypothesis b <> 0 was removed), making it essentially unusable in a development that should build both before and after 8.14. So, Z_div_mod_eq should not be deprecated until 8.17.

Doesn't that mean Z_div_mod_eq_full has the same type in 8.14 8.15 and 8.16 providing 3 consecutive versions where it can be used to avoid the deprecated Z_div_mod_eq?

---

This isn't the first time I've seen users ask for delayed deprecation, but I don't understand the logic. Understanding "deprecated" as "we intend to remove this", isn't it better to warn users as early as the decision is made?
Maybe we are lacking ways to more precisely control deprecation warnings, like for instance a way to ignore deprecations for 8.16+ but not 8.15?

[xavierleroy]

Doesn't that mean Z_div_mod_eq_full has the same type in 8.14 8.15 and 8.16

I think this is the case. Unless you change it before the final 8.16 release :-)

This isn't the first time I've seen users ask for delayed deprecation, but I don't understand the logic. Understanding "deprecated" as "we intend to remove this", isn't it better to warn users as early as the decision is made?

No. The replacement needs to be made available, advertised, tested and shown to be usable before the deprecation decision is taken and users are warned. For that, 3 major versions is a reasonable delay between introducing the replacement and adding the deprecation warning. That's more or less the policy we use for OCaml's standard library.

[Zimmi48]

Thank you in advance for putting a little more discipline and thoughts into stdlib deprecation warnings.

That's more or less the policy we use for OCaml's standard library.

Just FTR, this has never been Coq's compatibility policy (for reference cf. my thesis for instance), so what you are suggesting is to change our compatibility policy. This is fine, but should be noted, because it's not exactly the same kind of discussion to have as compared to if the compatibility policy had not been respected.

The replacement needs to be made available, advertised, tested and shown to be usable before the deprecation decision is taken and users are warned.

Interesting. It looks like you are distinguishing "advertised" and "warned". Usually, we warn because it is our best way to advertise a future change to users (although they have been cases when we knew our future replacement was not usable yet and we have used another strategy). What would you recommend as a good advertisement strategy?

EDIT: in response to:

This has been possible for quite a while now

FTR, you have been lucky, but this is because you don't use some of Coq's features. For instance, we have deprecated the use of the command Hint Rewrite without a locality in the version when we introduced support for the locality.

[Blaisorblade]

• Z_div_mod_eq is deprecated in 8.16 but its recommended replacement, Z_div_mod_eq_full, changed type between 8.13 and 8.14 (an hypothesis b <> 0 was removed), making it essentially unusable in a development that should build both before and after 8.14. So, Z_div_mod_eq should not be deprecated until 8.17.

FWIW, there is an officially documented solution — https://github.com/coq/coq/pull/14086/files#diff-22ee97be0b7ad32c2e0256009b1f07942cec570ca00b8a5c4faf11d468001dc2. It might still qualify as unusable.

[xavierleroy]

Usually, we warn because it is our best way to advertise a future change to users (although they have been cases when we knew our future replacement was not usable yet and we have used another strategy). What would you recommend as a good advertisement strategy?

For OCaml: usually it's just a mention in the Changes file, which is not much but better than nothing. We also have posts on discuss.ocaml.org highlighting the main novelties in a release; these are good conversation starters.

At any rate, warning may be the best advertisement, but only if the alternative is widely usable, i.e. has been available and working for several versions. Otherwise, the warning is not advertisement but an annoyance.

FTR, you have been lucky, but this is because you don't use some of Coq's features. For instance, we have deprecated the use of the command Hint Rewrite without a locality in the version when we introduced support for the locality.

Oh, I ran into this issue but it was possible to turn this specific warning off (deprecated-hint-rewrite-without-locality). For stdlib functions, I can't turn off specific deprecation warnings, it's either having all of them or none.

[Zimmi48]

Indeed, I don't think we are very good at communicating about our changelog and starting conversations about it. Maybe we should do more on this front.

Oh, I ran into this issue but it was possible to turn this specific warning off (deprecated-hint-rewrite-without-locality). For stdlib functions, I can't turn off specific deprecation warnings, it's either having all of them or none.

Thanks for pointing that out! That's indeed a serious issue. Maybe what Gaëtan was suggesting above would actually be an acceptable solution?

Maybe we are lacking ways to more precisely control deprecation warnings, like for instance a way to ignore deprecations for 8.16+ but not 8.15?

For instance, stdlib warnings already have the information of the version at which they were deprecated. We could add this information into the warning name to make it easy to disable all the recently introduced warnings. WDYT?