Théo Zimmermann (Nov 17 2020 at 09:58): Théo Zimmermann (Nov 17 2020 at 09:58):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.
Enrico Tassi (Nov 17 2020 at 19:59):I can update compat tomorrow.
For the rest we have a call tomorrow :smile:
Théo Zimmermann (Nov 18 2020 at 16:20):In the end, we forgot to talk about this.
Matthieu Sozeau (Nov 18 2020 at 18:24):Right. We'll do next week
Hugo Herbelin (May 31 2021 at 16:17):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?
Théo Zimmermann (May 31 2021 at 16:22):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.
Hugo Herbelin (May 31 2021 at 16:34):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.
Guillaume Melquiond (May 31 2021 at 16:59):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.)
Gaëtan Gilbert (May 31 2021 at 17:03):the other one is marked for 8.15 anyway
Guillaume Melquiond (May 31 2021 at 17:04):Indeed, my mistake.
Michael Soegtrop (May 31 2021 at 17:07):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.
Théo Zimmermann (Jun 01 2021 at 08:49):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).
Théo Zimmermann (Jun 01 2021 at 08:51):@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.
Michael Soegtrop (Jun 01 2021 at 09:31):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.
Hugo Herbelin (Jun 02 2021 at 07:51):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
Pierre-Marie Pédrot (Jun 07 2021 at 08:33):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?
Guillaume Melquiond (Jun 07 2021 at 08:39):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.
Pierre-Marie Pédrot (Jun 07 2021 at 08:41):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.
Pierre-Marie Pédrot (Jun 07 2021 at 08:41):Said otherwise, I am not sure I understand the new process.
Michael Soegtrop (Jun 07 2021 at 08:42):Can you say when you will do the branch?
Pierre-Marie Pédrot (Jun 07 2021 at 08:42):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.
Gaëtan Gilbert (Jun 07 2021 at 08:43):branching is what causes the freeze
do not freeze master
Pierre-Marie Pédrot (Jun 07 2021 at 08:44):uh? but we can't get random stuff into 8.14 though
Gaëtan Gilbert (Jun 07 2021 at 08:48):why not? it's not branched yet
Pierre-Marie Pédrot (Jun 07 2021 at 08:48):this is looking for trouble
Pierre-Marie Pédrot (Jun 07 2021 at 08:49):I don't want the poor RM to have to remove bits of PRs because we realize midway that something went wrong
Gaëtan Gilbert (Jun 07 2021 at 08:50):the same argument applies to PRs from a month ago
maybe we should never merge anything
Pierre-Marie Pédrot (Jun 07 2021 at 08:51):not true, because one month is enough to observe issues usually
Pierre-Marie Pédrot (Jun 07 2021 at 08:51):our CI is notably not complete in particular for dev-related stuff
Pierre-Marie Pédrot (Jun 07 2021 at 08:51):(e.g. we're still seeing problems from time to time with the dune transition although everything was green)
Guillaume Melquiond (Jun 07 2021 at 08:52):Okay, I will branch then, and I will postpone the 32 open pull requests to 8.15.
Pierre-Marie Pédrot (Jun 07 2021 at 08:54):most of the stuff I see in the milestone have zero chance of making it for 8.14
Pierre-Marie Pédrot (Jun 07 2021 at 08:55):there is one serious blocker though
Gaëtan Gilbert (Jun 07 2021 at 09:02):what blocker?
Pierre-Marie Pédrot (Jun 07 2021 at 09:03):https://github.com/coq/coq/issues/14306
Pierre-Marie Pédrot (Jun 07 2021 at 09:09):I've demilestoned a handful of PRs that, according to me, had no chance to make it.
Pierre-Marie Pédrot (Jun 07 2021 at 09:10):some of them didn't even build on the CI, and there is even a draft in there :
Michael Soegtrop (Jun 07 2021 at 09:10):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.
Pierre-Marie Pédrot (Jun 07 2021 at 09:11):half of the stuff in there are PRs blocked / in zombie state
Pierre-Marie Pédrot (Jun 07 2021 at 09:12):this is not magically going to be solved by shouting "freeze! freeze!" Balmer-style imo
Michael Soegtrop (Jun 07 2021 at 09:12):Well for those PRs the triaging should take 10s each. The other half is the interesting one.
Pierre-Marie Pédrot (Jun 07 2021 at 09:13):Yes, I've left PRs that should be easy to merge
Pierre-Marie Pédrot (Jun 07 2021 at 09:13):(even the draft one should probably be merged!)
Pierre-Marie Pédrot (Jun 07 2021 at 09:14):Relatedly, I'd like to see some statistics on PR merges.
Michael Soegtrop (Jun 07 2021 at 09:15):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.
Pierre-Marie Pédrot (Jun 07 2021 at 09:15):I suspect that there is an exponential distribution for time-to-merge
Pierre-Marie Pédrot (Jun 07 2021 at 09:15):with some filter above which a PR will never be merged and linger forever
Pierre-Marie Pédrot (Jun 07 2021 at 09:16):most of the long tail of PRs is sitting around without any movement
Michael Soegtrop (Jun 07 2021 at 09:16):I have some of these - but eventually it will get done.
Pierre-Marie Pédrot (Jun 07 2021 at 09:16):you're not in the leading board though
Michael Soegtrop (Jun 07 2021 at 09:20):You mean in the group participating in the triage meeting or the top 10 on the longterm PR statistics?
Pierre-Marie Pédrot (Jun 07 2021 at 09:20):in the longterm PR stats
Théo Zimmermann (Jun 07 2021 at 11:44):@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.
Cyril Cohen (Jul 07 2021 at 13:45):Hi, I assume the timeline on the wiki is outdated, do you have any update?
Guillaume Melquiond (Jul 07 2021 at 14:04):No, as long as there are blocker bugs for the release, it is hard to give any estimate.
Enrico Tassi (Jul 07 2021 at 14:08):I see 4 at least https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+milestone%3A8.14%2Brc1
Théo Zimmermann (Jul 07 2021 at 15:17):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?
Emilio Jesús Gallego Arias (Jul 07 2021 at 16:12):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]
Théo Zimmermann (Jul 20 2021 at 06:49):@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.
Théo Zimmermann (Jul 20 2021 at 06:50):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.
Théo Zimmermann (Jul 20 2021 at 06:52):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).
Michael Soegtrop (Jul 20 2021 at 08:03):I just wanted to ask (for the Coq Platform time planning) what the current schedule is.
Théo Zimmermann (Jul 20 2021 at 08:05):@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.
Guillaume Melquiond (Jul 20 2021 at 08:25):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.
Michael Soegtrop (Jul 20 2021 at 08:28):So since it is "just" change log surgery, the plan is still end of the month?
Guillaume Melquiond (Jul 20 2021 at 08:33):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.
Michael Soegtrop (Jul 20 2021 at 08:37):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".
Guillaume Melquiond (Jul 20 2021 at 08:42):That is right.
Théo Zimmermann (Jul 20 2021 at 08:47):@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?
Guillaume Melquiond (Jul 20 2021 at 08:53):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.
Hugo Herbelin (Jul 20 2021 at 08:56):@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.
Guillaume Melquiond (Jul 20 2021 at 08:59):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).
Ali Caglayan (Jul 20 2021 at 09:19):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.
Théo Zimmermann (Jan 13 2022 at 16:46):@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?
Guillaume Melquiond (Jan 13 2022 at 18:26):Fine with me.
Théo Zimmermann (Jan 13 2022 at 18:42):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