Gaëtan Gilbert (May 12 2022 at 15:31): Gaëtan Gilbert (May 12 2022 at 15:31):Is there much interest in a 8.15.2 release? See https://github.com/coq/coq/projects/46 for possible fixes to backport (note I haven't checked that they are actually backportable)
(related dates: 8.16 branching is coming up, 8.16.0 release expected in july)
Karl Palmskog (May 12 2022 at 15:32):if there's a chance that 8.16.0 will be delayed, e.g., due to vacation absences or other unforeseen issues, I think it would be a good idea to do 8.15.2
Karl Palmskog (May 12 2022 at 15:33):personally, I think 8.15 has been a great major release so far, and there are some changes that could lead to trouble, like the findlib thing, in 8.16. This might be an argument for 8.15.2.
Théo Zimmermann (May 12 2022 at 15:42):I think that CoqIDE-wise, @Jim Fehrle was hoping for an 8.15.2 release.
Guillaume Melquiond (May 12 2022 at 15:52):Honestly, I had to go back to 8.14, because 8.15 (even 8.15.1) is too awful to use with Coqide. (I haven't checked whether the queued-up changes are sufficient to bring 8.15 back to the quality of 8.14.)
Paolo Giarrusso (May 12 2022 at 18:56):I'll submit the 2 backports in https://github.com/Blaisorblade/coq/tree/v8.15-backports for consideration (I might be able to add them to the column, if that's okay?) — we're using them and one should be a straightforward performance improvement, while the other is a small semantic bugfix so it might be out of scope
Jim Fehrle (May 12 2022 at 19:54):I would do an 8.15.2 release for the CoqIDE issues. I've addressed the issues I've been able to reproduce. I haven't been able to reproduce the "coqidetop died" that @Pierre-Marie Pédrot mentioned on one of the recent Coq calls. Let's make sure we get all the important ones fixed in 8.15.2. Perhaps we could merge #15996 and #15992 and then have someone (@Guillaume Melquiond?) see if that's satisfactory.
Gaëtan Gilbert (May 12 2022 at 20:51):Paolo Giarrusso said:
I'll submit the 2 backports in https://github.com/Blaisorblade/coq/tree/v8.15-backports for consideration (I might be able to add them to the column, if that's okay?) — we're using them and one should be a straightforward performance improvement, while the other is a small semantic bugfix so it might be out of scope
I added the gc one
The primproj change is part bugfix part semantic change so not sure indeed
Michael Soegtrop (May 13 2022 at 06:21):Let me also check the CoqIDE/VsCoq parallelism issue discussed yesterday - I wanted to do some tests yesterday and didn't manage - will so so asap. To me this looks like a regression maybe even to 8.15.0 in 8.15.1.
Théo Zimmermann (May 17 2022 at 19:05):@Gaëtan Gilbert Did you make any decision regarding whether to prepare an 8.15.2 version?
Théo Zimmermann (May 25 2022 at 09:13):ping @Gaëtan Gilbert Any decision yet?
Gaëtan Gilbert (May 25 2022 at 12:56):let's do it
Théo Zimmermann (May 25 2022 at 12:59):OK let's briefly talk about this at the Coq Call then if we can.
Gaëtan Gilbert (May 31 2022 at 08:37):tagging when https://gitlab.com/coq/coq/-/pipelines/551905256 is done (assuming success)
Gaëtan Gilbert (May 31 2022 at 11:50):it is now tagged
@Karl Palmskog are you willing to do the opam packages for this version?
Michael Soegtrop (May 31 2022 at 12:02):I guess there should be a Coq Platform minor release as well.
Théo Zimmermann (May 31 2022 at 12:09):Yes, especially given how problematic some issues with CoqIDE have been for some users.
Tej Chajed (May 31 2022 at 12:24):I'd like to bring up https://github.com/coq/coq/issues/15891 - Coq hasn't been building from source in Homebrew for some time, due to a change in something upstream (even 8.15.0 no longer builds). Even if this isn't an issue in Coq per se, it is currently preventing upgrading the Homebrew formula.
Karl Palmskog (May 31 2022 at 14:53):@Gaëtan Gilbert thanks for the ping, I will do the opam packages for 8.15.2 tonight May 31 European time unless someone beats me to it
Last updated: Oct 03 2023 at 04:02 UTC