Stream: Coq devs & plugin devs

Topic: 8.14 release thread


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 17 2020 at 19:59):

I can update compat tomorrow.
For the rest we have a call tomorrow :smile:

view this post on Zulip Théo Zimmermann (Nov 18 2020 at 16:20):

In the end, we forgot to talk about this.

view this post on Zulip Matthieu Sozeau (Nov 18 2020 at 18:24):

Right. We'll do next week

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Gaëtan Gilbert (May 31 2021 at 17:03):

the other one is marked for 8.15 anyway

view this post on Zulip Guillaume Melquiond (May 31 2021 at 17:04):

Indeed, my mistake.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 08:41):

Said otherwise, I am not sure I understand the new process.

view this post on Zulip Michael Soegtrop (Jun 07 2021 at 08:42):

Can you say when you will do the branch?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jun 07 2021 at 08:43):

branching is what causes the freeze
do not freeze master

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 08:44):

uh? but we can't get random stuff into 8.14 though

view this post on Zulip Gaëtan Gilbert (Jun 07 2021 at 08:48):

why not? it's not branched yet

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 08:48):

this is looking for trouble

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 08:51):

not true, because one month is enough to observe issues usually

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 08:51):

our CI is notably not complete in particular for dev-related stuff

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 08:55):

there is one serious blocker though

view this post on Zulip Gaëtan Gilbert (Jun 07 2021 at 09:02):

what blocker?

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:03):

https://github.com/coq/coq/issues/14306

view this post on Zulip 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.

view this post on Zulip 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 :

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:11):

half of the stuff in there are PRs blocked / in zombie state

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:13):

Yes, I've left PRs that should be easy to merge

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:13):

(even the draft one should probably be merged!)

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:14):

Relatedly, I'd like to see some statistics on PR merges.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:15):

I suspect that there is an exponential distribution for time-to-merge

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:15):

with some filter above which a PR will never be merged and linger forever

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:16):

most of the long tail of PRs is sitting around without any movement

view this post on Zulip Michael Soegtrop (Jun 07 2021 at 09:16):

I have some of these - but eventually it will get done.

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:16):

you're not in the leading board though

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jun 07 2021 at 09:20):

in the longterm PR stats

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Jul 07 2021 at 13:45):

Hi, I assume the timeline on the wiki is outdated, do you have any update?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Michael Soegtrop (Jul 20 2021 at 08:03):

I just wanted to ask (for the Coq Platform time planning) what the current schedule is.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jul 20 2021 at 08:28):

So since it is "just" change log surgery, the plan is still end of the month?

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip Guillaume Melquiond (Jul 20 2021 at 08:42):

That is right.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.


Last updated: Oct 21 2021 at 21:03 UTC