Plan for backwards compatibility and deprecation

[langston-barrett]

First of all, I'm excited about this effort. As a new Coq user, it can be very difficult to figure out which aspects of the standard library reflect current best practices, and which are in an old style.

I think this project will be most successful if it is explicit about when it's releases will start being backwards compatible with themselves (v1.0, basically). When this happens, it would be good to have a thorough, long term plan for implementing breaking changes (how to warn users, how long things stay deprecated, etc).

Note that I'm referring to internal backwards compatibility, not compatibility with, say, Coq's current stdlib.

[maximedenes]

That's a very good point! In fact, I've been working recently on deprecation mechanisms, see for instance rocq-prover/rocq#7907

I hope we can implement something similar for lemmas and definitions, but it requires some careful design.

And indeed, I hope to communicate clearly what stages the project is expected to go through, making it clear when it stabilizes. For now, I'm really working on the infrastructure, so a preliminary step.

[langston-barrett]

See also rocq-prover/rocq#6043

[gares]

A related scenario to be considered is the following one that just arose in math-comp.
It is about moving a lemma L from a library X to the stdlib.
In our case it is some lemmas/defs from the new finfun.v file into ssrfun.v (part of Coq nowadays).

In math-comp we try to be nice with users and support two versions of Coq, so until L is in Coq we can hardly integrate finmap. What we can do is to have the extra lemmas in finmap, and also in Coq eventually, and remove the copy in finmap when L has been sitting in Coq for 2 releases. Having duplicate definitions is not 100% OK since (eve if they are convertible) they can be distinguished by tactics (eg the matching machinery of rewrite).

It could help to push the idea of -compat 8.x further and have an attribute to filter out a command
when a constraint on the Coq version is met. For example

Module Compat810. stuff. End Compat810.
#[ coq-older("8.10")] Export Compat810.

In this way duplication could be avoided (and the -compat flag probably be replaced by the same machinery as well). In any case this "path" from an external library to Coq's stdlib2 should be considered, and should be something that does not break the library you pull stuff from.

CC @CohenCyril