A different approach to handling backward compatibility?

[charguer]

When I read the discussion on the plan for update for the "global vs export" behavior for hints requiring users to edit all their files ( https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140/5 ), when I take into consideration legacy features such as "Set Implicit Arguments" polluting all the files, and when I recall all the nice improvement ideas that have been effectively unable to make it to Coq due to the (legitimate) concern of not breaking backward compatibility in a hard-and-painful manner, I keep coming back to this idea of having a totally-different look at the treatment of backward compatibility.

Concretely, when compiling a Coq file, the user specifies, either as argument to coqc, or as a meta information at the first line of the file, what is the behavior of Coq to simulate. (Generally, adding a version argument to the Makefile could be simpler, but for a project aggregating files from different places, it might be convenient to allow attaching a version number to each file.)

The release of version "n" would support behaviors for major releases in the range "n-2" to "n". This means, assuming a major release every 1 year, that the author of a stable, not-actively-developed library can update is file once every 3 years, and still maintain a working library to all the community, whichever version of Coq users are using. Even for Coq actively-developed libraries, it would be very useful to allow distinguishing between (a) the time at which the package compiles in the most recent release of Coq, and (b) the time at which the author(s) find the time to update the code to the default behaviors of the latest release of Coq.

Coq developers are free to totally drop support for version n-3, allowing them to perform code cleanup on a regular basis, and not stick for ever with legacy features / flag settings.

For making a backward-incompatible change, there is no need to go through several phases over several years (deprecated/error/silently-gone). Instead, the change (e.g. changing the default value of a flag, changing the behavior of a tactic in a corner case) would apply immediately, by default, in the release that introduces it.

Moreover, there is a way to reduce the effort for a user to migrate one file from one version to the next version. A release of Coq (and this release only) would support flags to select, for each backward-incompatible feature, whether to consider the prior behavior or the new behavior. It is a bit like activating/deactivating warnings, except that in this case it activates/deactivates new behaviors. Allowing to fix proof scripts by fixing issues one by one would save a considerable amount of effort to the user. Indeed, when one change is considered at once, there is no need for the user to figure out which change is breaking the script, it can only be that one. Overall, this would make script update much easier, even in the face of several backward-incompatible changes.

How much effort would that put on the Coq developers? The code base would feature a record storing the "transition flags", with their respective values for version n-2, n-1 and n. Where a piece of code sees its behavior modified, the code can branch based on the selected value of the transition flag. Upon a new release of Coq, the transition flags are shifted. At some point, for changes that become 3 releases old, the values of the flag become identical for all versions. At this point, the branching in the code may be removed, and the legacy code cleaned up.

If you like the proposed approach, or if you think that it is totally stupid, please let me know.

[ejgallego]

We already are supposed to have something like that, but it is opt-in AFAICT [by the Coq.Compat modules]

[charguer]

We already are supposed to have something like that, but it is opt-in AFAICT [by the Coq.Compat modules]

Interesting. Is this documented? For which features is this used? What obstacles to leveraging this version mechanism such as the treatment of "Global/export" status of hints? What is the associated promise in term of number of years of support?

Is there a possibility to require these compatibility modules from the compilation line, just like -open would do in OCaml to load a module as if it was a line at the head of the source file?

[ppedrot]

That's the -compat option...

[ppedrot]

What obstacles to leveraging this version mechanism such as the treatment of "Global/export" status of hints?

We can simply switch off the warning in the 8.13 compat file? I don't see any difference with your proposal.

[charguer]

Well, the good new is that some part of the necessary back-end is already implemented, and that other person seem to share the same interest as me in using compatibility versions.

Yet, there remains numerous questions:

• what is the guidelines for changes that can be implemented directly, and compatibility supported via -compat, v.s. changes that need to a depreciation warning in one release before a change is made?
• what is the associated promise in term of number of years of support for -compat?
• amazing, I've never heard about -compat although it exists since 8.2, and have read a fair numer of change logs... is its use discouraged so much to the point of not advertizing it at the head of the changes.html documentation? how many library developers ever relied on "Require compat..."?

[Zimmi48]

Yes, -compat is documented. It is used whenever a breaking change is introduced with a compatibility flag. Then, the flag is set in the Compat module so that the old behavior is emulated when the right -compat flag is passed on the command line. We could indeed complete this Compat module with some warning disabling if people think it makes sense.

[Zimmi48]

what is the guidelines for changes that can be implemented directly, and compatibility supported via -compat, v.s. changes that need to a depreciation warning in one release before a change is made?

There's no clear guideline but let's say it depends on the scale of the impact. If a very major breaking change happens immediately with a compatibility flag to unset it, users will be bothered, because they will need to figure out what the cause of the change is (or that they need to use the -compat flag, which not a lot of users do). Also, unfortunately, we have too few users carefully reading the changelog.

what is the associated promise in term of number of years of support for -compat?

OTOH, there's a clear guideline for this question, to the point that the compat infrastructure is automatically updated using dedicated scripts. We keep compatibility with the last two stable releases IIRC.

[Zimmi48]

The use of -compat is not discouraged, but it's true that we didn't advertise it much recently and I think very few users are relying on it. We could decide to advertise it more...

[charguer]

Following a video chat with @Zimmi48, and further thoughts, here are a few additional comments:

*) The "-compat" flag would be nothing be an alias for a list of flags controlling individual changes. For example, say 8.12 makes two backward-incompatible changes A and B w.r.t. 8.11, and that 8.13 makes one backward-incompatible chagnes w.r.t. 8.12. Then,

• coq-8.13/bin/coqc -compat 8.11 is equivalent to coq-8.13/bin/coqc -compatflags A,B,C, and it should presumably be able to compile all files that coq-8.11/bin/coqc can process.
• coq-8.13/bin/coqc -compat 8.12 is equivalent to coq-8.13/bin/coqc -compatflags A,B and it should presumably be able to compile all files that coq-8.12/bin/coqc can process.
• coq-8.13/bin/coqc -compat 8.13 is equivalent to coq-8.13/bin/coqc

*) In particular, if a user wants a robust Makefile for compiling a bunch of proof scripts developed for 8.12 in a way that does not depend on the exact version of Coq installed on the system, it is possible to use coqc -compat 8.12 as compilation line in the Makefile.

*) Allowing to turn-off an individual non-backward-compatible feature introduced in a given release of Coq is particularly useful when the implementation of that feature turns out to have a bug or an unexpected interaction with other features. This has happened numerous times in the past. With the current approach, one is forced to wait for the next release of Coq, and there is potentially no way to get the development to work with certain releases. For example, CFML2 could not compile on Coq8.10 and Coq8.11, and could not benefit from any of the features from these two releases, until a change in typeclasses resolution was fixed in 8.12. On the contrary, with the option to individually turn on or off backward-incompatible changes, I could have compiled my development using the right options throughout every release.

*) Coq users have been used for over a decade to particular effort from the developers in not breaking backward compatibility at once. This is very kind for users but it comes at the cost of slowing down patches to the current design, something that is ultimately not the wish of users. What I'm suggesting is to make a move towards a different philosophy: any given release might break a bunch of behaviors, however there is the guarantee that files can be compiled using the option "-compat N-1".

*) There remains the question of the usefulness of warnings.

• It is certainly useful to issue warnings of the form "this compatibility option will no longer be available in the next release of Coq". Those are for features that changed in version N-2 and that remain exploited by the user at version N of Coq.
• Then there are warnings of the form "the use of this feature is deprecated and will be removed at the next release". One may think they have some usefulness. But if the next release and the following ones are still able to emulate that feature, what is the point of telling users that the feature will be removed in the future, as opposed to removing it right away? Users who wish to continue using the deprecated feature (and would have been happy to turn off the warning) could simply use the compatibility flag associated with that particular feature to continue using it.

*) Last but not least, compatibility flags could and should be used for experimental features, which could be turned off by default. The current situation is that experimental features go in a release and are available by default. This causes serious issues when, as mentioned earlier on, the new features has unexpected interactions with existing ones. Thus, it would be much nicer than experimental features (i.e. more than a minor patch) can be first tested by volunteers who would explicitly turn on a flag. (Flags such as type-in-type also belong to this category of "flags off by default", although this specific option will never become "on by default".)

Remark with respect to this last point: the beta-release phase is usually too short to discover all problematic interactions: it allows discovering the first problematic interaction, but by the time this first one is fixed, it is time for the release and the second problematic interaction is missed. On the contrary, an experimental feature could be finely tested, patched and tuned accross an entire major release. Also, it would make it very clear for users that a feature is experimental and there is no promise whatsoever as to maintain any form of backward compatibility with respect to that particular feature until it becomes packaged by default.

[charguer]

@ejgallego rightfully points out the question of whether there should be backward-compatible support for bugfixes. This is a good question.

• For bugs introduced in experimental features (that are off by default), clearly there is no need (see comment above).
• For bugs introduced in features that have been around for some time, I would tend to say that it is needed. Because the scripts of the users take the bug into account. Say a tactic leaves an hypothesis that it should have cleared in a specific case. Changing that behavior will break the user scripts. To me, the interest of the compat flag only holds if we can provide full compatibility.

From an implementation point of view, all the minor bug fixes associated with a specific release could be covered by a flag named, says, minor-bugfixes-of-8.12. When fixing a bug in the code base, rather than replacing the code, the developer would do a switch over the value of that flag to consider either the old code or the patched one. After 2 years, the legacy code can be removed.

[CohenCyril]

This reminds me of protocols which datagrams start with declaring the version number of the protocol at use. Would it make sense that coq --behaviour=8.x (where 8.x is an alias for several single behaviours that could be listed instead as @charguer suggests) is the default way of using coq? EDIT: Maybe it should actually be in the header of a file, or a library...

[Blaisorblade]

As a relevant “testcase”, would this policy unblock something like Unifall?

[charguer]

One additional question is whether plugins could benefit from a similar methodology. Would it be the case that each plugin can export its custom list of compatibility flags? And, for plugin developers that find backward compatibility too hard to maintain, there should be a standard manner to issue a warning to the user that requests compatibility via -compat that the plugin does not guarantee backward compatibility.

[Zimmi48]

@CohenCyril

This reminds me of protocols which datagrams start with declaring the version number of the protocol at use. Would it make sense that coq --behaviour=8.x (where 8.x is an alias for several single behaviours that could be listed instead as @charguer suggests) is the default way of using coq?

How would that be different from -compat= exactly?

@charguer

coq-8.13/bin/coqc -compat 8.11 is equivalent to coq-8.13/bin/coqc -compatflags A,B,C

As we discussed, this would already be possible with the features we have today but your -compatflags is actually a bunch of -set and -unset (see documentation).

@charguer

To me, the interest of the compat flag only holds if we can provide full compatibility.

Then it's a deal-breaker. On the one hand, you defend that we should move forward faster, but if on the other hand you intend for compat flags to be introduced for every bug fix in non-experimental features, this is going to be way too hard to apply in practice. What we can do though, is to distinguish two kinds of bug fixes: the ones that are considered low impact (and for which we didn't need an overlay in our CI), which are currently shipped in patch-level releases, and the ones which are considered high impact which are only shipped in major releases. It would be reasonable to expect to introduce compat options for the latter more often, but I'm not even sure this would be reasonable to do systematically.

@charguer

Would it be the case that each plugin can export its custom list of compatibility flags?

Again, with the current features, plugin / library authors can advertise a list of -set / -unset that users can put on the command-line flag (or the corresponding Set / Unset that they can put in a specific file) to emulate the previous behavior.

[Zimmi48]

As I said to @charguer, if we wish to go this way, the proposal should first go through a CEP. The interested parties will meet during CUDW to discuss this topic and the hypothetical CEP. Coordination should happen here: https://coq.zulipchat.com/#narrow/stream/255971-CUDW-2020/topic/WG.3A.20Backward.20Compatibility

[charguer]

To me, the interest of the compat flag only holds if we can provide full compatibility.

You're right to point out that this may be too strong. I should have written: "if we can provide compatibility for every high-impact changes". That would probably be good enough, and much better than the current situation. We're fine for users to spend a little bit of time at each migration, as long as we allow them to postpone the time at which they need to make big changes.

plugin / library authors can advertise a list of -set

What we may want to take into account is that -compat 8.12 should be an alias for a list of flags, and this list should include the compatibility flags associated with the plugins that are loaded.

[Zimmi48]

Currently, -compat 8.12 is an alias for -require-import Compat812, which itself is just a file setting a bunch of flags, and therefore, it can be replaced by a bunch of -set to set the corresponding flags on the command line. I think leaving it open to the plugin maintainers to follow a similar compatibility policy should be very much possible with the current feature set. However, trying to make -compat 8.12 more powerful and also tackle the issue of external plugins is (IMHO): 1. much more complex; 2. not flexible enough for plugin writers, which may release major versions with breaking changes without keeping in sync with Coq's own release cycle.