Stream: Coq devs & plugin devs

Topic: Backporting policy


view this post on Zulip Janno (Aug 26 2021 at 13:33):

What's the general policy for backporting changes to point releases? There are quite a few performance-relevant changes slated to go into 8.15. The ones I followed (dnet related, mostly) seemed like they could go into 8.14.1 without introducing problems. With the release schedule for 8.14 being quite a bit behind (correct?) I suppose 8.15 is not happening anytime soon. So I am interested in the possibility of backporting these changes.

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 14:06):

If they could go into 8.14.1, they could just as well go to 8.14.0 since it isn't ready yet. Just ping the RM to ask his opinion on relevant PRs (@silene).

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 14:07):

As for 8.15, it is not clear it will be delayed. Last time a release was late (8.9) the next one happened just three months after.

view this post on Zulip Vincent Laporte (Aug 26 2021 at 14:59):

I also wonder about currently released versions: can bug fixed in 8.14 still be backported to 8.13?

view this post on Zulip Lasse (Aug 26 2021 at 15:04):

I should note that I do maintain a personal repo where I backport relevant fixes for myself all the way back to 8.10

view this post on Zulip Paolo Giarrusso (Aug 26 2021 at 22:43):

I think one of those changes fixes a user-visible bug with dnet inference (Pierre-Marie's eta-reduction in TC search), so it might be _more_ suitable in 8.14.0 than 8.14.1.

view this post on Zulip Janno (Aug 27 2021 at 08:47):

That's a good point. I had suggested 8.14.1 to avoid delaying 8.14.0 in any way.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 14:01):

To remove the "maybe", I'll note that making try apply _. succeed more often (which happens with that patch) is a breaking change, which Coq tries to avoid in point releases. I _conjecture_ that if you can supply the backport and it doesn't break CI too much, it shouldn't delay things.

view this post on Zulip Hugo Herbelin (Aug 27 2021 at 15:24):

Lasse said:

I should note that I do maintain a personal repo where I backport relevant fixes for myself all the way back to 8.10

Interesting, then maybe could this be announced somewhere (or even PR-ed to the relevant branches)?

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:36):

I've backported some fixes myself but with today's "expensive" releases, PRs might be rejected because there's no release coming. If, OTOH, releases were just tags that pass CI, PRs would make more sense.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:37):

... some backports might still break compatibility, strictly speaking, but for those announces would make sense.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:47):

Or one could just allow such fixes.

For instance, https://github.com/Blaisorblade/coq/commit/7c85aec48efff57cb43d8df9410c8d88e3a5f64d backports to 8.13 a bugfix that makes TC search less incomplete, so technically it could break some clients.

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:49):

I'd be a bit wary about backporting these patches. They're introducing observable differences in parts that are very hard to control, and it's not because the CI is impervious to the changes that there is no code in the wild that exploit the bug.

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:50):

We have (had?) basically no spec for pattern filtering so it's hard to frame them as "bugs" actually.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:51):

Would you object to adding them to 8.14.0-rc1, or to earlier releases?

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:52):

I am not the RM, who is sovereign, but if I were I wouldn't include them.

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:52):

also the code is not stable yet, I am still writing fine-tuning patches atop of this so it'd be better to get everything at once

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:53):

without insisting, can I ask why? I understand the last point, but not the earlier one.

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:54):

Is the idea that outside projects test against the 8.14 branch, and would have time to catch incompatibilities?

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:56):

my main fear is that auto tactics are intricate blackboxes that people routinely call without checking the traces

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:56):

that's absolutely true :-).

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:56):

even while preserving backwards compat it's unclear we wouldn't hit performance issues, for instance

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:57):

of the kind that are very hard to fix

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:57):

because that means reworking your whole set of hints

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:57):

but without testing, that seems a (valid) argument against ever changing TC search behavior

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:58):

if people never test anything before the RC, merging 1 day before the RC or merging 90 day is equally unsafe.

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:58):

well, maybe I'm just too cautious

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 16:59):

I mean, I agree it's a great question, and it'd be great if everybody did the testing that invalidates my argument :-).

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:59):

but then this still counts as an argument against backporting in 8.14.1

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 16:59):

it we backport it, we must backport it now

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 17:00):

absolutely! or even backporting after the 8.14.0-RC1 :-)

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 17:01):

then your judgment about instability matters, but that's for you (and @Janno who's testing these backports) to evaluate

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 17:04):

(and the RM of course)

view this post on Zulip Paolo Giarrusso (Aug 27 2021 at 17:05):

(also I haven't discussed with Janno and asked him what he thinks — even if we work together)

view this post on Zulip Pierre-Marie Pédrot (Aug 27 2021 at 17:11):

(since it seems we're a hurry, I'm taking advantage of this thread to veer slightly off-topic to signal that https://github.com/coq/coq/pull/14788 has been waiting for a bit and is still waiting for an assignee...)

view this post on Zulip Lasse (Aug 28 2021 at 11:12):

Hugo Herbelin said:

Interesting, then maybe could this be announced somewhere (or even PR-ed to the relevant branches)?

It may be useful to have some branches in the main Coq repo where people can backport possibly slightly incompatible PR's to older versions. Probably not with the purpose of creating a formal release, but just to merge everyone's efforts.

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 13:17):

@Pierre-Marie Pédrot if @Janno has time, would his review help?

view this post on Zulip Théo Zimmermann (Aug 28 2021 at 16:04):

Lasse said:

Hugo Herbelin said:

Interesting, then maybe could this be announced somewhere (or even PR-ed to the relevant branches)?

It may be useful to have some branches in the main Coq repo where people can backport possibly slightly incompatible PR's to older versions. Probably not with the purpose of creating a formal release, but just to merge everyone's efforts.

To avoid confusion, I would avoid doing this in the main Coq repo. But this seems like a good fit for a repo that would belong in the coq-community organization...

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 17:20):

:+1: — especially since many won't care for such strict compatibility (I'm unsure myself)


Last updated: Oct 16 2021 at 02:03 UTC