Coq: Which models for evolving while maintaining compatibility?

[herbelin]

As recommended by @zimmi48, I copy here a digression started in PR #876 about compatibility. See e.g. also #915 (fix to rewrite in *) or #991 (unifall) for other bits of discussion.

Two questions

• how to allow compatibility internally and to which extent?
• what user-level model(s) to support compatibility?

Supporting compatibility models internally

In an absolute compatibility-preserving model, every little change would come protected by an internal flag which deactivates the change under some compatibility mode, and this independently of the user-level model for changes, i.e. independently of whether there is a specific user-level flag, a per-tactic versioning, a per-release versioning of the whole set of tactics, etc.

But such absolute-compatibility-preserving model might eventually lead to obfuscated code, with,

• either eventually a lot of if version N then bla else foo in it, with progressive obfuscation, difficulty to have a code easy to read for newcomers, etc.
• or, in case we radically duplicate code, to duplication of maintenance work, difficulties to keep code synchronous, etc,

So maybe, instead of looking for an absolute model, one could make an evaluation change by change of whether it is worth supporting different behaviors.

Different user-level possible models

1. do we continue to propose a model of individual flags with a risk of proliferation which makes things more and more complicated?
2. do we move to tactic-based versioning?
3. do we move to a global versioning of the set of tactics?
4. do we recommend a model of ifdef in Coq files?
5. a mix of those?

What was @mattam82 proposing? Was it more 2. or 3.?

Also, do we continue a policy of deprecation basically expecting users to update their development at latest every 2 years? On one side, this is necessary for reducing the maintenance load for developers, on the other side, this is taking the risk of loosing developments whose updating would be too costly. I must confess that I'm a bit all at sea ("dans le brouillard") wrt these questions.

[Zimmi48]

First, thanks for raising this issue. I think it is important to have this discussion even if the conclusion is "we don't know what is best yet, let's try a few approaches".

As you mention, 1 (a model of individual flags) is the "legacy" solution but because we haven't yet really switched to any other model, we have continued to use this model, even in 8.8.

The risk of proliferation / obfuscation is currently avoided with the new policy of deprecation, that is a compatibility option introduced in version 8.x is deprecated in version 8.(x+1) and removed in version 8.(x+2) unless some users complain. But this means that there is still a maintenance burden for users, with some "grace period".

In the short term, this deprecation model is very useful to conduct important clean-up in the code of Coq and does not introduce such a big maintenance burden because of our careful evaluation of compatibility issues.

Longer term, I don't think that we should keep this deprecation policy. What I have in mind instead is that we switch to semantic versioning starting with Coq 9.0. This would mean e.g. publishing a new major (as in X.0.0) version every two years, with three intermediate minor (as in X.Y.0, Y != 0) versions, released every six months, with one or two intermediate patch-level (as in X.Y.Z, Z != 0) versions. The minor versions would preserve backward-compatibility as much as possible but could introduce new features, new options and deprecate stuff. And of course, the patch-level versions would not introduce new features, as is the case today. The actual removal of deprecated stuff and the changes in default option values would only happen at the time of the major release, once every two years. Note that I'm not suggesting that we enact this policy for the next release or the one after, but since I have had this on my mind for some time, I thought I'd share it and this issue was the right place since it asked about the deprecation policy.

I'm not opposed to 2 & 3 (tactic-versioning) provided that we see how to do it. I'm not opposed either to 5 if it helps testing various approaches.

Finally a solution to consider is the one currently experimented for Ltac2 or considered for the Standard Library 2.0: develop the new thing outside of the Coq source tree, get it tested, and integrate it much later, when it has stabilized (possibly replacing quickly what was there before).

[herbelin]

I'm not opposed to 2 & 3 (tactic-versioning) provided that we see how to do it.

For 3. (global versioning), this is somehow already available in the sense that new options setting by default to a change of behavior and introduced in version X.Y are deactivated when option -compat X.Z with Z<Y is given. This means (assuming this is generalized, which is easy) that (for those changes about which we evaluated that an option was needed, but potentially also for changes not bound to an option), setting -compat (or an equivalent vernac side, say Set Compat X.Z) places you (globally) in the semantics of X.Z.

For 2. (per-tactics versioning), it is some infrastructure to provide (e.g. adding a node SetVersion in tactic_expr) and some user-level syntax to provide (e.g. version X.Z in ...) but it is certainly possible, with the same internal version-protected flags as above.

In both cases, the worries that I see (and remember) are:

• the static vs dynamic effect of versioning: if I have a tactical foo defined in X.Y used in a X'.Y'context, does foo behaves like X.Y, or like X'.Y', or like X.Y for the static part of foo but like for X'.Y' for the arguments supplied to foo? This was discussed somewhere, but I don't remember where at the current time.

The actual removal of deprecated stuff and the changes in default option values would only happen at the time of the major release, once every two years.

Basically, the question here is: do we want to allow a user having started a development in version X.Y.Z to extend his development with files written in X+1.Y'.Z' without having to upgrade his/her X files? I.e., having major release number would work as a clear signal that some compatibility is broken but that would still mean having to upgrade the whole database of code on which we are working at latest every two years if one wants to take benefit of the features... but maybe this is also a reasonable deal, it is difficult to judge.

Otherwise, having a model where each tactics come equipped with a list of documented options and each version comes with a list of which of the documented options are set in this version, is a model which is possible from my point of view. With a good documentation, this will probably be acceptable for users (beginners or casual users would just use the default configuration, expert users will fine-tuned the semantics accordingly to their need). What holds me back is that I feel that most developers seem to consider that Coq is already too complex.

So, it seems there is really a compromise to find between different needs. What others do think?

[ejgallego]

I will try to summarize some of my thoughts and discussions over the past couple of years.

First, I think there may be two separate issues here:

• to detect unintended compatibility problems
• to manage intended compatibility changes.

The Travis infrastructure was developed to help with the first point, and so far is doing a fine job. IMHO it is safe to assume that developments not wanting to join Travis are assumed to deal with breakage on their own. [An additional problem is large efforts such as Verdi, for which we need to setup GitLab's CI]

Evidence has proven we are not good a predicting breakage, but the situation is quite better now so I think we can safely focus on point 2.

In this second point there is IMO a clear distinction between the consumers of the ML-API vs the consumers of LTAC.

For the first, I feel that the in-tree vs out-of-tree discussion is not yet closed, Coq has tried in the past some interesting efforts such as coq-contribs, and some models such as the one used in Linux (in-tree drivers) or in Jane Street (a single large repos) seem to favor the "monolitic" way to manage compatibility.

Regarding .v files, I think the best option is to try to migrate and avoid the introduction of compatibility structures and technical debt. We have shown this is possible up to a certain extent, and IMO it should be the favored approch.

Compatibility support should IMO be introduced in very concrete cases. For example unification / tactics is a good example.

Another key point that large changes such as unifall open is that the opportunity to break compatibility is usually a good moment to do other changes. This is similar to the semantic versioning @Zimmi48 proposes.

Regarding Hugo's questions:

how to allow compatibility internally and to which extent?

IMO we should avoid introducing compatibility code as much as possible.

what user-level model(s) to support compatibility?

Users should try to track the latest Coq version if possible.

do we continue to propose a model of individual flags with a risk of proliferation which makes things more and more complicated?

For the reasons you point out, we should avoid this model as much as we can.

do we move to tactic-based versioning?
do we move to a global versioning of the set of tactics?

Global versioning seems right. It is IMO difficult to reason about individual tactics in isolation of others.

do we recommend a model of ifdef in Coq files?

IMO we should avoid that too. We should remove any incentives for users wanting to stay in old Coq version. For instance, now that we are avoiding unintended compatibility problems, users can migrate much more easily.

[SkySkimmer]

do we recommend a model of ifdef in Coq files?

IMO we should avoid that too. We should remove any incentives for users wanting to stay in old Coq version. For instance, now that we are avoiding unintended compatibility problems, users can migrate much more easily.

OTOH for the HoTT patch for #1033 I used crazy ltac stuff to preserve backwards compatibility. It certainly felt like ifdef would have been cleaner.

[maximedenes]

Closing this issue for now, but feel free to reopen if more brainstorming is needed.