Deprecation deletion overwriting · Coq devs & plugin devs

As far as I know the delay for considering the deletion of a statement in Coq stdlib (or other Coq features) after deprecation is at least two Coq versions.
In the case, for example, of an improvement of a statement (by weakening some hypothesis) or of trying to free a name for a more appropriate alternative statement, this could lead to:

This might be a bit long but in the opposite too short for projects interested in compability with older versions of Coq (as pointed by @Guillaume Melquiond for example the current Debian version is 8.12.0), see coq/coq#16920 for concrete examples with projects in Coq CI (by the way some Coq CI projects trigger lots of deprecation warnings).

Is there a best practice? what kind of solution can be settled to provide better backward compatibility? and possibly avoiding moving back and forth between name and name'?

Guillaume Melquiond (Nov 28 2022 at 09:57):

Note that I am not advocating for a longer deprecation period, as long as there exists a suitable replacement that makes it possible to preserve backward compatibility. The issue is when this replacement appears at the exact same time as the deprecation rather than predating it. In that case, it becomes tedious to support multiple versions of Coq. In fact, there might even be a period of time where it becomes impossible to compile a library without any deprecation warning, which rightfully aggravates users, e.g., https://github.com/coq/coq/issues/16287

Olivier Laurent (Nov 28 2022 at 10:08):

If I understand correctly what you mean, it is not the case with the 4-versions process above.
Concerning backward compatibility, this is one of the key problems for me. I do not know how to deal with these kinds of replacements name -> name' -> name in a backward compatible way. As suggested by @Jason Gross, inlining could be a solution in very simple cases, but I don't think it scales.

Jason Gross (Nov 28 2022 at 11:53):

You can also add name' in a backwards compatibility module and Require Import that in the relevant places.

Olivier Laurent (Dec 10 2022 at 16:53):

@Jason Gross Are you referring to the compat infrastructure? If so are those modules alive for more than 2 versions?
Moreover in any case, it is not clear to me how to use modules to deal with a situation where:

Jason Gross (Dec 10 2022 at 17:27):

Suppose you have Coq.Foo.Bar.name. You can write the following backwards compatible code:

Require Import Coq.Foo.Bar.
Module Coq. Module Foo. Module Bar.
Notation name := tt (only parsing).
Notation name' := Coq.Foo.Bar.name (only parsing).
End Bar. End Foo. End Coq.
Notation name := Coq.Foo.Bar.name' (only parsing).

In versions of Coq with name', the notation will refer to Coq's version of name'. In other cases, it will refer to Coq's version of name, if it exists. If neither exists, it'll refer to tt.

Andres Erbsen (Dec 10 2022 at 17:48):

For yet another strategy, I believe Ltac2.Env can query whether definitions exist by name. I expect it would work in a Definition, not sure about Notation.

Andres Erbsen (Dec 10 2022 at 17:57):

Notation tt := ltac2:(
  Control.refine (fun _ => Env.instantiate (Control.plus
  (fun _ => Option.get_bt (Env.get [@Coq;@Compat;@Coq10;@Coq;@Init;@Datatypes;@tt]))
  (fun _ => Option.get_bt (Env.get [@Coq;@Init;@Datatypes;@tt]))))).

Gaëtan Gilbert (Dec 10 2022 at 18:03):

Andres Erbsen (Dec 10 2022 at 18:03):

However, I am not sure whether we want anything this fancy: perhaps it makes more sense to adapt developments that depend on an old version of a lemma so that they Import the relevant Compat file after the file that contains the Lemma.

Gaëtan Gilbert (Dec 10 2022 at 18:04):

I think if you're willing to modify the development the easiest way to be backwards compatible is to vendor the new version until you drop compat with the old coq
or vendor the old version as you prefer

Andres Erbsen (Dec 10 2022 at 18:07):

Yes, for small changes this makes sense. And if we are looking at removing or changing a definition or lemma, eventually the development will need to be changed anyway. The suggestion to use a Compat file instead of copy-paste vendoring is solely to reduce reviewer effort in downstream developments.

Jason Gross (Dec 10 2022 at 18:09):

Andres Erbsen (Dec 10 2022 at 18:23):

Further, if we're confident that whatever compat solution we arrive at works, I'd be in favor of just making the change in Coq (and CI developments) without a deprecation delay. This would require non-CI developments to apply the compat solution when upgrading to the changed Coq version, without flexibility to defer resolving a warning (so the required changes would really need to be very easy). However, they would gain the option to switch to the new definition right away and thus reduce the total amount of work they need to do comparison to the rename-remove-rename-remove strategy. For changes that may be difficult to adapt to, like the omega->lia transition, a deprecation cycle is obviously warranted.

Stream: Coq devs & plugin devs

Topic: Deprecation deletion overwriting

Olivier Laurent (Nov 28 2022 at 08:40):