Stream: Coq devs & plugin devs

Topic: Deprecation deletion overwriting


view this post on Zulip Olivier Laurent (Nov 28 2022 at 08:40):

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'?

view this post on Zulip 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

view this post on Zulip Olivier Laurent (Nov 28 2022 at 10:08):

The issue is when this replacement appears at the exact same time as the deprecation rather than predating it.

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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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]))))).

view this post on Zulip Gaëtan Gilbert (Dec 10 2022 at 18:03):

Or just Notation tt := ltac:(exact one || exact the_other)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jason Gross (Dec 10 2022 at 18:09):

Or just Notation tt := ltac:(exact one || exact the_other)

This will break once https://github.com/coq/coq/pull/16935 is merged though

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 10 2022 at 18:35):

Jason Gross said:

Or just Notation tt := ltac:(exact one || exact the_other)

This will break once https://github.com/coq/coq/pull/16935 is merged though

if it's merged


Last updated: Feb 02 2023 at 13:03 UTC