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:

- deprecate
`name`

in version n (and introduce new/stronger statement as`name'`

) - delete
`name`

in version n+2 (and rename`name'`

as`name`

, deprecate`name'`

) - delete
`name'`

in version n+4

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

?

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

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.

You can also add `name'`

in a backwards compatibility module and `Require Import`

that in the relevant places.

@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:

`name`

was used for statement`A -> B`

in version`n`

`name`

is used for statement`B`

(or`A' -> B`

with`A -> A'`

) in version`m`

>`n`

(or the new statement is`name'`

which is fresh wrt version`n`

and possibly`name`

does not exist anymore in version`m`

)- one wants compatibility with both version
`n`

and version`m`

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`

.

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.

```
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]))))).
```

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

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.

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

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.

Or just

`Notation tt := ltac:(exact one || exact the_other)`

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

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.

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: Sep 15 2024 at 13:02 UTC