Stream: Coq users

Topic: 8.15.2?


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

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

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

view this post on Zulip Théo Zimmermann (May 12 2022 at 15:42):

I think that CoqIDE-wise, @Jim Fehrle was hoping for an 8.15.2 release.

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (May 25 2022 at 09:13):

ping @Gaëtan Gilbert Any decision yet?

view this post on Zulip Gaëtan Gilbert (May 25 2022 at 12:56):

let's do it

view this post on Zulip Théo Zimmermann (May 25 2022 at 12:59):

OK let's briefly talk about this at the Coq Call then if we can.

view this post on Zulip Gaëtan Gilbert (May 31 2022 at 08:37):

tagging when https://gitlab.com/coq/coq/-/pipelines/551905256 is done (assuming success)

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

view this post on Zulip Michael Soegtrop (May 31 2022 at 12:02):

I guess there should be a Coq Platform minor release as well.

view this post on Zulip Théo Zimmermann (May 31 2022 at 12:09):

Yes, especially given how problematic some issues with CoqIDE have been for some users.

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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC