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.
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
).
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.
I also wonder about currently released versions: can bug fixed in 8.14 still be backported to 8.13?
I should note that I do maintain a personal repo where I backport relevant fixes for myself all the way back to 8.10
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.
That's a good point. I had suggested 8.14.1 to avoid delaying 8.14.0 in any way.
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.
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)?
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.
... some backports might still break compatibility, strictly speaking, but for those announces would make sense.
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.
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.
We have (had?) basically no spec for pattern filtering so it's hard to frame them as "bugs" actually.
Would you object to adding them to 8.14.0-rc1, or to earlier releases?
I am not the RM, who is sovereign, but if I were I wouldn't include them.
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
without insisting, can I ask why? I understand the last point, but not the earlier one.
Is the idea that outside projects test against the 8.14 branch, and would have time to catch incompatibilities?
my main fear is that auto tactics are intricate blackboxes that people routinely call without checking the traces
that's absolutely true :-).
even while preserving backwards compat it's unclear we wouldn't hit performance issues, for instance
of the kind that are very hard to fix
because that means reworking your whole set of hints
but without testing, that seems a (valid) argument against ever changing TC search behavior
if people never test anything before the RC, merging 1 day before the RC or merging 90 day is equally unsafe.
well, maybe I'm just too cautious
I mean, I agree it's a great question, and it'd be great if everybody did the testing that invalidates my argument :-).
but then this still counts as an argument against backporting in 8.14.1
it we backport it, we must backport it now
absolutely! or even backporting after the 8.14.0-RC1 :-)
then your judgment about instability matters, but that's for you (and @Janno who's testing these backports) to evaluate
(and the RM of course)
(also I haven't discussed with Janno and asked him what he thinks — even if we work together)
(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...)
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.
@Pierre-Marie Pédrot if @Janno has time, would his review help?
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...
:+1: — especially since many won't care for such strict compatibility (I'm unsure myself)
Last updated: Oct 13 2024 at 01:02 UTC