Dear RM, I have updated the milestones in my PRs, and kept to 8.13 only those I think that make sense; BR.
Thanks
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
it's the same, branching means freezing (with very little exceptions for PR which are backported)
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?
That's probably a good idea!
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?
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.
@Hugo Herbelin please send me a list of PRs that you need assignee for 8.13
The ones that are already assigned to me, I will process on time
I just moved the ones still in progress to 8.14. The list for 8.13 (20 PRs) is here. A few remarks:
destruct
; to merge if there is support for itThanks a lot in advance!
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?
BTW you can add coq/coq in front of a PR number to make it clickable. Example: coq/coq#13025.
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!)
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).
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.
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.
@Enrico Tassi That's important and useful info. Thanks!
@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!
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.
If I'll need guidance, I'll ask. So far so good, with the big "?" about pinnig cs/installer/platform.
Sure, no problem. I did create the project before making the branch
Btw, you did help on many PRs today, without even asking you... thanks
I'll call this a day ;-)
Quite a long day indeed, phew. :beers:
@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.
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!
that's a bit unfortunate, but thanks for looking into it
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
@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.
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.
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?
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?
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?
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
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.
Here it is : https://github.com/coq/bignums/pull/50
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.
I was not talking about the bignums CI but the Docker-Coq pipelines actually.
@Enrico Tassi , you need to put the 8.14+alpha tag in the repos so git describe
works again.
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.
ok, on it
https://github.com/coq/coq/pull/13457
Is there already a planned release date for 8.13?
We have this small wiki page https://github.com/coq/coq/wiki/Release-Plan
@Emilio Jesús Gallego Arias : thanks - I put it on my Coq important link list :-)
Did I miss another stream talking about 8.13? In any case, congratulations for the announcement, I'm joigning Enrico to express pride.
Yes, congrats to everyone involved and thanks to Enrico in particular!
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
Can you say more? Do you have explicit match constructs around?
Did you change the scope of hints in response to a new warning?
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
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?
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.
@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?
That would be great, thanks
Done
Last updated: Oct 13 2024 at 01:02 UTC