Stream: Coq devs & plugin devs

Topic: 8.13 release thread


view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2020 at 22:59):

Dear RM, I have updated the milestones in my PRs, and kept to 8.13 only those I think that make sense; BR.

view this post on Zulip Enrico Tassi (Nov 06 2020 at 08:07):

Thanks

view this post on Zulip Karl Palmskog (Nov 06 2020 at 08:11):

when is the v8.13 branch estimated to be created? I can never remember if that coincides with the freeze or if it's later

view this post on Zulip Enrico Tassi (Nov 06 2020 at 08:35):

it's the same, branching means freezing (with very little exceptions for PR which are backported)

view this post on Zulip Hugo Herbelin (Nov 11 2020 at 18:10):

Hi, do we add a 8.14+alpha (or whatever syntax it should have)? I guess that unless they are urgent, new PRs should start target 8.14?

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 08:09):

That's probably a good idea!

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 08:54):

Emilio Jesús Gallego Arias said:

Dear RM, I have updated the milestones in my PRs, and kept to 8.13 only those I think that make sense; BR.

By the way, the time needed to treat PRs which are ready, or ready up to minor fixes, should be accounted in the schedule. Has someone an overview at the number of such open PRs yet to treat?

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 09:06):

I've just removed all my own PRs but one from the milestone. But clearly, there's a lot of stuff in there, that doesn't belong here anymore because it's clearly not ready yet.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2020 at 14:50):

@Hugo Herbelin please send me a list of PRs that you need assignee for 8.13

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2020 at 14:50):

The ones that are already assigned to me, I will process on time

view this post on Zulip Hugo Herbelin (Nov 12 2020 at 22:44):

I just moved the ones still in progress to 8.14. The list for 8.13 (20 PRs) is here. A few remarks:

Thanks a lot in advance!

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 07:59):

it would be easier to merge #13025 since 8.12 has already a fix, but otherwise the 8.12 patch (#13073) can be backported instead

It's not called backporting in this case. Rather forward porting. But it was already done. Didn't you see my comment about that?

view this post on Zulip Théo Zimmermann (Nov 13 2020 at 07:59):

BTW you can add coq/coq in front of a PR number to make it clickable. Example: coq/coq#13025.

view this post on Zulip Hugo Herbelin (Nov 13 2020 at 09:56):

Théo Zimmermann said:

It's not called backporting in this case. Rather forward porting. But it was already done. Didn't you see my comment about that?

I saw but not realized what it implied, sorry. So, let's postpone coq/coq#13025 for simplicity. (And yes, forward porting would be better!)

view this post on Zulip Hugo Herbelin (Nov 16 2020 at 08:19):

The freeze is planned today and there are about 50 PRs targetting 8.13+beta. I can participate to live PR merge sessions during the week if ever it can facilitate interactions and contribute to manage the load (for today, tomorrow or Wednesday, it can be for instance from 5pm).

view this post on Zulip Enrico Tassi (Nov 16 2020 at 09:15):

My plan is to branch this afternoon. Meanwhile I plan to organize all existing PR targeting the beta in a GH project so to have a list of PR which were there before the fork. After the branching I'll only consider backporting PRs from that list (or documentation changes or important fixes).

Please don't rush merging code just because it is in the beta milestone. Reverting broken code can be quite some work. Finally there is nothing bad if some code code will be in for 8.14: when one opens a PR he clearly picks the next beta as a milestone, but this does not mean that it has to be absolutely merged before that deadline, just that it should be considered. Or at least, this is the meaning I intend to give to the label, and I'll do my best to give all these PR a look.

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

I've done a rough count excluding the bug fixes and documentation PRs (which are usually not concerned by the freeze) and the PRs which are clearly not in a state that's ready for 8.13 and only half (25 PRs) remained.

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

@Enrico Tassi That's important and useful info. Thanks!

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

@Enrico Tassi I told Maxime that I would help on some steps like creating the backport project but apparently you didn't need my help. That's great!

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

The two PRs that were added to the "Request inclusion" column can be explained by their merge into master. The bot didn't know that the branching had not yet happened.

view this post on Zulip Enrico Tassi (Nov 16 2020 at 17:54):

If I'll need guidance, I'll ask. So far so good, with the big "?" about pinnig cs/installer/platform.

view this post on Zulip Enrico Tassi (Nov 16 2020 at 17:54):

Sure, no problem. I did create the project before making the branch

view this post on Zulip Enrico Tassi (Nov 16 2020 at 17:55):

Btw, you did help on many PRs today, without even asking you... thanks

view this post on Zulip Enrico Tassi (Nov 16 2020 at 17:56):

I'll call this a day ;-)

view this post on Zulip Hugo Herbelin (Nov 16 2020 at 19:47):

Quite a long day indeed, phew. :beers:

view this post on Zulip Karl Palmskog (Nov 17 2020 at 12:50):

@Erik Martin-Dorel Given that I add the usual coq.8.13.dev package in core-dev, can you add an 8.13 Docker nightly image as before? Would help a ton with testing 8.13 on our armada of projects in coq-community and elsewhere.

view this post on Zulip Erik Martin-Dorel (Nov 20 2020 at 23:22):

Hi @Karl Palmskog sure, thanks for the ping, I'll look after this ASAP!
Actually this won't be straightforward anymore until I push a new version of docker-keeper because with the help of @Théo Zimmermann, we replaced the nightly builds (for coqorg/coq:dev) with an immediate trigger through GitLab CI with a dedicated pipeline variable… and this does not support multi-branches for the moment. But, this is definitely on my TODO list, and I hope this will be ready next week!

view this post on Zulip Karl Palmskog (Nov 20 2020 at 23:23):

that's a bit unfortunate, but thanks for looking into it

view this post on Zulip Erik Martin-Dorel (Nov 20 2020 at 23:28):

Yes, that recent improvement makes the setup more tricky... but in the end, we'll get fully up-to-date alpha images, with more updates than just nightly deployments :)
I'll keep you informed anyway

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 12:09):

@Erik Martin-Dorel The GitLab webhook trigger on the Coq repo is currently set up for the master branch only. I think we will need to add one per active release branch. So let me know when I should do this.

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 12:09):

BTW @Erik Martin-Dorel it seems that the current build for master is failing during the bignums step since the recent merge of the native compute flag PR.

view this post on Zulip Erik Martin-Dorel (Nov 22 2020 at 12:32):

Théo Zimmermann said:

BTW it seems that the current build for master is failing during the bignums step since the recent merge of the native compute flag PR.

indeed, do you talk about this failure? https://travis-ci.com/github/coq/bignums/jobs/445358441 − which seems to only occur with Nix.

IIUC, this comes from that line: https://github.com/coq/bignums/blob/master/Makefile.coq.local#L2
while Nix/coq-on-cachix wouldn't currently install the .coq-native/* files… However I'm puzzled by this error, as it should probably have occurred before the merge of https://github.com/coq/coq/pull/13352 (?)

So do you know whether it's coq or bignums that should be fixed to avoid this?

view this post on Zulip Erik Martin-Dorel (Nov 22 2020 at 12:37):

OK, I think I understand (Cc @Pierre Roux FYI): before #13352, the default -native-compiler flag of Coq did install the .coq-native/* files for Coq's stdlib.
But now, the default option (-native-compiler ondemand) doesn't precompile the stdlib, so in bignums CI, -native-compiler yes raises a failure. To fix this, we might want to pass the -native-compiler yes flag to Nix… Do you agree with this? if yes, do you know where this option could be configured?

view this post on Zulip Erik Martin-Dorel (Nov 22 2020 at 12:43):

Otherwise, maybe it's better to keep the default -native-compiler ondemand flag in Nix (to fully preserve backward compatibility - modulo the mere stdlib precompilation), so we could just replace -native-compiler yes with -native-compiler ondemand in bignums to fix this, which would thereby be a bignums issue, not a coq issue… WDYT?

view this post on Zulip Erik Martin-Dorel (Nov 22 2020 at 13:13):

OK so I'm definitely convinced it was just a bignums issue and I've opened a PR: https://github.com/coq/bignums/pull/49

view this post on Zulip Pierre Roux (Nov 22 2020 at 13:17):

Erik Martin-Dorel said:

To fix this, we might want to pass the -native-compiler yes flag to Nix… Do you agree with this? if yes, do you know where this option could be configured?

I'd rather fix bignums, let me open a PR there.

view this post on Zulip Pierre Roux (Nov 22 2020 at 13:25):

Here it is : https://github.com/coq/bignums/pull/50

view this post on Zulip Erik Martin-Dorel (Nov 22 2020 at 13:26):

Thanks @Pierre Roux, I agree with you and I had already opened PR #49 BTW :) but I will close it as you PR is more complete.

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

I was not talking about the bignums CI but the Docker-Coq pipelines actually.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 23 2020 at 15:17):

@Enrico Tassi , you need to put the 8.14+alpha tag in the repos so git describe works again.

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 15:33):

Not just this but also this:

Change the version name to the next major version and the magic numbers (see #7008).

Additionally, in the same commit, update the compatibility infrastructure, which consists of invoking dev/tools/update-compat.py with the --master flag.

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 15:33):

See also https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/8.2E14.20release.20thread

view this post on Zulip Enrico Tassi (Nov 23 2020 at 15:40):

ok, on it

view this post on Zulip Enrico Tassi (Nov 23 2020 at 15:48):

https://github.com/coq/coq/pull/13457

view this post on Zulip Michael Soegtrop (Nov 23 2020 at 16:47):

Is there already a planned release date for 8.13?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 23 2020 at 16:57):

We have this small wiki page https://github.com/coq/coq/wiki/Release-Plan

view this post on Zulip Michael Soegtrop (Nov 23 2020 at 17:01):

@Emilio Jesús Gallego Arias : thanks - I put it on my Coq important link list :-)

view this post on Zulip Hugo Herbelin (Dec 08 2020 at 21:55):

Did I miss another stream talking about 8.13? In any case, congratulations for the announcement, I'm joigning Enrico to express pride.

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 22:29):

Yes, congrats to everyone involved and thanks to Enrico in particular!

view this post on Zulip Karl Palmskog (Dec 21 2020 at 15:14):

hmm, I'm seeing quite different behavior between 8.12 and 8.13+beta1 in typeclass resolution (inside a section with Context). Is this to be expected? I don't see anything particular about this in the changelog

view this post on Zulip Enrico Tassi (Dec 21 2020 at 15:46):

Can you say more? Do you have explicit match constructs around?

view this post on Zulip Enrico Tassi (Dec 21 2020 at 15:46):

Did you change the scope of hints in response to a new warning?

view this post on Zulip Karl Palmskog (Dec 21 2020 at 15:49):

hmm, I didn't change much of anything in the project which I have problems porting to 8.13. But if it's not something obvious, I might spend some time minimizing the example. I think was able to rule out it has something to do with Instance Generalized Output at least

view this post on Zulip Karl Palmskog (Dec 21 2020 at 15:50):

I did change a bunch of Hint X to Global Hint X, but per pmp's guide, I think this is the recommended thing to do?

view this post on Zulip Karl Palmskog (Dec 21 2020 at 15:52):

intuition for what is happening: suddenly a bunch of TC instances declared with Context are not found when they are needed in 8.13. Unfortunately the bug minimizer will take hours, so will have to do a manual minimization.

view this post on Zulip Théo Zimmermann (Jan 06 2021 at 11:43):

@Enrico Tassi There should probably be a milestone for 8.13.1 so that PRs can start being added to it. Do you want me to create it and the corresponding project columns?

view this post on Zulip Enrico Tassi (Jan 06 2021 at 11:43):

That would be great, thanks

view this post on Zulip Théo Zimmermann (Jan 06 2021 at 11:48):

Done


Last updated: Oct 15 2021 at 21:02 UTC