We need to nominate one or two RMs for 8.14, bump the version number in master
and run the first part of the compat infrastructure update for 8.14.
I can update compat tomorrow.
For the rest we have a call tomorrow :smile:
In the end, we forgot to talk about this.
Right. We'll do next week
Hi, is this the thread to talk about the 8.14 release? Is the feature freeze still happening today? I forgot how it should be interpreted and where the release notes are? Does this mean no new 8.14/8.13.3 PRs from today? Does this mean a decision to take within 2 weeks about each currently opened 8.13.3/8.14 PR?
Does this mean a decision to take within 2 weeks about each currently opened 8.13.3/8.14 PR?
Not at all. This means that when @Guillaume Melquiond pushes the branch (which he didn't do yet), virtually no (unmerged) feature PR will get into 8.14.
Is there a way to clarify where efforts have to be made so that ready PRs can go in 8.14? In the meantime, I'm going to do a pass on my PRs to postpone those not ready.
I do not have time today, and I presumably will not have time tomorrow either, so the branching will not happen before Wednesday. Anyway, I might delay branching as long as https://github.com/coq/coq/issues/14306 is open, since it is a real blocker for the release. (I do not consider the other one to be an actual blocker.)
the other one is marked for 8.15 anyway
Indeed, my mistake.
Théo Zimmermann said:
Not at all. This means that when Guillaume Melquiond pushes the branch (which he didn't do yet), virtually no (unmerged) feature PR will get into 8.14.
It would be nice to merge all PRs which are ready to merge and marked as 8.14 before the branch (e.g. #14293), though. I would also say that everything which is marked 8.14 and was in review for > 2 weeks with only minor short notice review changes should get some triaging.
Indeed, but for this we would need reviewers to get mobilized, which wasn't really done this time (probably because the RM himself wasn't available in the weeks before the freeze).
@Hugo Herbelin Besides postponing some of your own PRs, I would recommend making sure that you didn't leave any PR that is ready with a pending review request from you, and that you merge any PR that is ready to merge of which you are the main reviewer and/or assignee.
Well we will see - my PR was reviews by Guillaume, so I guess he will merge. It is just cleanup but I want to avoid that the "cleanup worthy" things I did with the constructive reals in 8.13 (putting a lot of Q lemmas with ad hoc names into a single "hidden" file) get any more time to spread into user developments.
Théo Zimmermann said:
Hugo Herbelin Besides postponing some of your own PRs, I would recommend making sure that you didn't leave any PR that is ready with a pending review request from you, and that you merge any PR that is ready to merge of which you are the main reviewer and/or assignee.
Fair remark!
I have 45 requests for reviews on open PRs. My current policy is generally not to intervene on a PR if it is highly discussed and the process of reviewing goes well. One reason for doing so is that I feel my action would probably be redundant with what others already said. Another is that reading a long thread and getting a fair opinion of a discussion is rather time-consuming. Yet another reason is that I don't really necessarily feel enough expert to make valuable comments.
some details
What's the exact process for merging PRs in master now? Since we're in an impending freeze, I believe that we should refrain from merging anything until we get fresh news from @Guillaume Melquiond, right?
Yes, I would much prefer that people focus on reviewing currently open pull requests (or just postpone them). I have no intention of manually moving pull requests to the 8.14 branch, so any pull request that is not quickly processed will just be delayed to 8.15.
My question was quite in the other direction, I don't think we should merge anything new in 8.14 but in the meantime since there is no actual 8.14 branch that means we can't merge anything into master without facing potential issues.
Said otherwise, I am not sure I understand the new process.
Can you say when you will do the branch?
Before we would branch quickly and backport during the beta, but now it seems we're back to a situation where we have a large timeframe where master is untouchable.
branching is what causes the freeze
do not freeze master
uh? but we can't get random stuff into 8.14 though
why not? it's not branched yet
this is looking for trouble
I don't want the poor RM to have to remove bits of PRs because we realize midway that something went wrong
the same argument applies to PRs from a month ago
maybe we should never merge anything
not true, because one month is enough to observe issues usually
our CI is notably not complete in particular for dev-related stuff
(e.g. we're still seeing problems from time to time with the dune transition although everything was green)
Okay, I will branch then, and I will postpone the 32 open pull requests to 8.15.
most of the stuff I see in the milestone have zero chance of making it for 8.14
there is one serious blocker though
what blocker?
https://github.com/coq/coq/issues/14306
I've demilestoned a handful of PRs that, according to me, had no chance to make it.
some of them didn't even build on the CI, and there is even a draft in there :
My suggestion would be to branch at a pretty much predefined date (with a bit of flexibility) and then be a bit more flexible on what to merge over. Some PRs are important and easy to merge. I would think that up to a few weeks after the merge, most PRs are trivial to merge. I would say for the PRs marked as 8.14 there should be some sort of triaging - maybe in the Coq call.
half of the stuff in there are PRs blocked / in zombie state
this is not magically going to be solved by shouting "freeze! freeze!" Balmer-style imo
Well for those PRs the triaging should take 10s each. The other half is the interesting one.
Yes, I've left PRs that should be easy to merge
(even the draft one should probably be merged!)
Relatedly, I'd like to see some statistics on PR merges.
IMHO branch at time X + triage what is left is the most sensible option. Of cause there should be a strict time limit on when these PRs are ready then, say 2 weeks. But the triage call should be right after the branch, so that people know what to concentrate on.
I suspect that there is an exponential distribution for time-to-merge
with some filter above which a PR will never be merged and linger forever
most of the long tail of PRs is sitting around without any movement
I have some of these - but eventually it will get done.
you're not in the leading board though
You mean in the group participating in the triage meeting or the top 10 on the longterm PR statistics?
in the longterm PR stats
@Guillaume Melquiond I agree that you shouldn't bother with new features and clean-ups after branching. But I hope that you're not shy at backporting trivial bug fix and documentation PRs that require no effort.
Hi, I assume the timeline on the wiki is outdated, do you have any update?
No, as long as there are blocker bugs for the release, it is hard to give any estimate.
I see 4 at least https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+milestone%3A8.14%2Brc1
So this was discussed in the call IIUC (sorry I missed the beginning because of a seminar at the same time). What was the conclusion? @Emilio Jesús Gallego Arias will take care of fixing them? Or we should do a release without a fix?
I will indeed submit a fix, but overall, at least for the bugs I'm concerned, are quite far from blockers [except maybe for the fake_ide one]
@Hugo Herbelin What's up with this 8.14.1 milestone? Between, 8.14+rc1 and 8.14.1, there is supposed to be 8.14.0 (so I'm renaming the milestone). Furthermore, while it's fine to add a milestone in the future for issues, if PRs are merged in this milestone at the moment, they will be ignored from the backporting process.
As far as I can tell, 8.14+rc1 is not going to be tagged anytime soon since there are still blocking issues that are not fixed.
But if we get closer to this point and it starts to make sense to milestone newly merged PRs for 8.14.0, then we need to adjust the Coq 8.14 project's columns so that 8.14.0 PRs are recorded (let me know @Guillaume Melquiond when you want this to happen / or if you want to take care of it yourself).
I just wanted to ask (for the Coq Platform time planning) what the current schedule is.
@Guillaume Melquiond said he hoped to release before the end of the month. But there are still two blocking issues https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+milestone%3A8.14%2Brc1+label%3A%22priority%3A+blocker%22 which are waiting on @Emilio Jesús Gallego Arias (at the very least to provide guidance regarding what should be done). So I'm not sure the release will happen in this time frame. If not, I'm afraid it might be delayed for a few more weeks.
As far as I am concerned, there are only two pull requests that are left to backport. The only reason I have not done so already is because they require some changelog surgery.
By the way, if you really want to backport such pull requests, please consult with me before, because it is just a pain.
As for the 8.14.0 milestone, I intend to reserve it purely for packaging/installing issues that are discovered in the release candidate. So, it does not make sense to assign existing pull requests to it.
So since it is "just" change log surgery, the plan is still end of the month?
As Théo explained, there are still blocker bugs. I just meant to say that these blocker bugs are the only things really delaying the release. But I cannot predict how and when they will be resolved.
Ah ok, I misunderstood your previous post then - I understood it such that you are correcting Théo's view and not adding to it. So the bottom line is more or less "asap but unknown".
That is right.
@Guillaume Melquiond Changelog surgery for PRs to backport should happen in the form of other PRs on master
. Otherwise, we get an inconsistency in the state of master
relative to the v8.14
branch. Do you want me to prepare a PR for these problematic changelog entries?
No, I will do it. I am just waiting the last minute, so that I can deal with all of them in a single pull request.
@Guillaume Melquiond : About #14610 and #14652 (which are in the inclusion request and have a change log), they could easily go to 8.14.1 if that's simpler. #14444 and #14542 (error reporting fixes w/o a change log) are more crucial for 8.14+rc1/8.14.0 in my view.
No, I am fine with them in 8.14.0. In fact, I have already pushed them on my branch. It is just that their changelogs are not in the proper place (and targeting 8.14.1 will not improve this issue in any way).
Emilio still has some unanswered questions in #14515 which aims to fix the blocker #14468. I think he is asking what the install prefix for the devel profile should be.
@Guillaume Melquiond I guess that now that 8.15.0 has been released, we can definitely say that there will be no 8.14.2 release, right? Can I take care of moving all the 8.14.2 PRs in the relevant 8.15 milestone (to reflect where they ended up appearing) and close the Coq 8.14 backport project?
Fine with me.
Done. Also note this comment that you could have missed: https://github.com/coq/coq/pull/15050#issuecomment-998807668
(I don't know how important this PR is though. Maybe another solution is to just close it.)
Last updated: Dec 07 2023 at 11:02 UTC