Stream: Coq Platform devs & users

Topic: 2022.04 release ready


view this post on Zulip Michael Soegtrop (Apr 05 2022 at 08:30):

I just did my final merge on the 2022.04 release. Please have a look. If nobody finds some obvious issue, I will tag today evening.

view this post on Zulip Julien Puydt (Apr 06 2022 at 05:20):

I updated my comparison page to follow the corresponding csv description.

view this post on Zulip Michael Soegtrop (Apr 06 2022 at 12:01):

I created the tag and a draft release. I will take care of the macOS signing.
@Enrico Tassi : can you please request the new Snap version (however they call it)
@Gaëtan Gilbert: can you please take care of the Windows installer signing? You can take the unsigned ones from here: (https://github.com/coq/platform/actions/runs/2094929601)

view this post on Zulip Enrico Tassi (Apr 06 2022 at 14:57):

Here: https://forum.snapcraft.io/t/2022-04-track-creation-for-coq-prover/29453

view this post on Zulip Michael Soegtrop (Apr 06 2022 at 15:36):

I took a note of how to request a new track, so that next time I am hopefully able to do it myself.

view this post on Zulip Enrico Tassi (Apr 11 2022 at 08:38):

The signed files are here: https://filesender.renater.fr/?s=download&token=0d31c227-c6cd-44bc-a2ef-7032e30e74d6

view this post on Zulip Michael Soegtrop (Apr 11 2022 at 09:02):

I will test and upload them later today.

view this post on Zulip Théo Zimmermann (Apr 19 2022 at 09:07):

Don't forget about the packages (if you haven't downloaded them yet). These links have expiration dates.

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:11):

@Théo Zimmermann : thanks! I already downloaded them but didn't have time to test them as yet - on plan for today.

view this post on Zulip Michael Soegtrop (Apr 20 2022 at 17:31):

@Enrico Tassi : can you have a look at the snap? I followed my notes and promoted the 2022.04.0 build to the latest and 2022.04 track and updated the landing page, but nothing of this is visible in the snap store for coq.

view this post on Zulip Michael Soegtrop (Apr 20 2022 at 17:36):

@Enrico Tassi @Théo Zimmermann @Gaëtan Gilbert : I just put the release online. Can one of you do the announcement in the various channels?

view this post on Zulip Michael Soegtrop (Apr 20 2022 at 17:39):

@Enrico Tassi : the snap issue is solved - it just seems to take 15 minutes or so (or maybe a web caching issue).

view this post on Zulip Théo Zimmermann (Apr 20 2022 at 17:47):

I can take care of this tomorrow.

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

Dear Coq community,

On behalf of the Coq development team, the release manager of Coq 8.15, and the Coq Platform team, we are happy to announce the immediate availability of the Coq Platform version 2022.04.0.

Release highlights:

The main supported version is:

Several compatibility collections with Coq 8.12 to 8.14 are available.

You may install the Coq Platform using opam-based scripts, or Windows, macOS and Snap binary installers (Coq 8.14 and 8.15 are available in the Windows and macOS installers, and only 8.15 in the Snap installer).

To learn about the Coq Platform and get access to the installers, please refer to:

https://github.com/coq/platform/releases/tag/2022.04.0

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:26):

Also, a question: shouldn't Flocq4 be among the release highlights (both in the announcement and on GitHub)? It surprises me that it is only mentioned in the notes.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:27):

you could mention Ott as well (but speaking in my own interest I guess)

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:27):

Sure. I didn't want to reproduce the full list of added packages and didn't know what to select.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:28):

I agree on the Flocq4 thing, though, that's a big change to a core package, and we can also mention that people should start to upgrade to it, although Flocq3 will be available for a while

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:29):

Théo Zimmermann said:

Sure. I didn't want to reproduce the full list of added packages and didn't know what to select.

I've now added the two that were added in "full mode".

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:29):

was Gaëtan alone as RM of 8.15?

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:29):

I think so.

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:30):

although Flocq3 will be available for a while

That's unclear though, isn't it? If CompCert and VST are compatible with Flocq 4 for the next (major) Platform release, we might drop Flocq3.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:30):

we don't have a policy for this, but I would have expected some deprecation policy like Coq's, i.e., Flocq3 becomes deprecated next Platform, then disappears in the one after the next

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:32):

I think we do have a policy: it is that Flocq 3 should remain available in the compatibility package picks (forever or for a long time) but not in the main pick...

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:32):

(Similarly to how we upgrade Coq at each major release but keep compatibility picks with older Coq versions.)

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:34):

I was at least under the impression that we wanted packages to carry forward to "main" by default

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:35):

so in my view, if Flocq3 will disappear in the next release main pick (for 8.16), then it should be signalled now

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:36):

@Michael Soegtrop so do you think you will retire Flocq3 for 8.16.0 pick?

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:36):

We could say "It is expected that the Flocq3 package will be removed when CompCert and VST become compatible with Flocq 4." to signal the removal intent without committing to a specific release.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:37):

sounds good to me, unless Michael has another proposal

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:46):

@Karl Palmskog : in the release notes here (https://github.com/coq/platform/releases) Ott os mentioned as major enhancement.

I must admit I didn't look at Flocq4 as yet, so I don't know how large the difference to Flocq3 is and if this qualifies as major enhancement. But I guess it would make sense to mention it anyway, so that people are aware.

Regarding the removal of Flocq3: My plan was to indeed remove it in the 8.16 release (Andrew and Xavier expressed their intention to make CompCert and VST Flocq4 compatible until then, but can't guarantee it). But I would also say that we ensure that there is a compatible opam package (which was btw. the main reason to name it Flocq3 and Flocq and not Flocq and Flocq4) for those who need it.

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:48):

I must admit I didn't look at Flocq4 as yet, so I don't know how large the difference to Flocq3 is and if this qualifies as major enhancement. But I guess it would make sense to mention it anyway, so that people are aware.

Major enhancement or not, it certainly is a major change since it's harder to port existing projects to it.

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:49):

@Michael Soegtrop Do you agree with the current form of the release announcement proposal (above)?

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:49):

And do you agree to add an item on Flocq4 in the release highlights on GitHub? (Should I do it?)

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:49):

Yes. I will add a section "major version changes" under hightlights.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:50):

Your text looks good to me. Since the list oof new packages is short, one could just mention it as a list (one liner).

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:52):

@Guillaume Melquiond : could you write a one liner what is new in Flocq4? IMHO it looks a bit silly to just write "we updated Flocq from version 3 to 4".

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:53):

(I know this is hard ...)

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:54):

it looks a bit silly to just write "we updated Flocq from version 3 to 4"

Is it? This is what we do for Coq itself, isn't it?

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:55):

One could also redirect to the Flocq 4 changelog. It's actually pretty short:

Version 4.0.0

made Coq 8.12 the minimal version and removed the IEEE754.SpecFloatCompat layer
removed automatic export of ZArith and Reals from Core.Raux and Core.Core

proved a close/far-path adder in Calc.Plus

made IEEE754.Binary a wrapper around IEEE754.BinarySingleNaN

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:55):

Well yes, but I guess more users of Coq Platform read the release notes of Coq than those of Flocq. Of course I would appreciate a 1..5 liner for Coq as well.

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 12:56):

For Coq, the best would be to put a direct link to the release highlights that are already available as an introduction to the changelog rather than copying them or shortening them even more.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 12:56):

I think it's good to emphasize the incompatibility between Flocq3 and 4 (for some serious cases, as per CompCert/VST)

view this post on Zulip Guillaume Melquiond (Apr 21 2022 at 12:56):

And actually, the only meaningful part is the last line: IEEE754.Binary is now a wrapper around IEEE754.BinarySingleNaN. If not for it, it would have been Flocq 3.5. Nothing was actually added to Flocq 4.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:58):

How about having a separate "Major changes" section?

view this post on Zulip Guillaume Melquiond (Apr 21 2022 at 12:59):

And the incompatibility is really minor. It is just that it is painful to make CompCert compatible with both Flocq 3 and Flocq 4 at the same time.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 12:59):

@Guillaume Melquiond : could you describe in a few words, what the benefits of this change are?

view this post on Zulip Guillaume Melquiond (Apr 21 2022 at 12:59):

For the user? None.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:00):

I can confirm that my own Flocq based code didn't require changes besides a few module/name things. It took me hardly 5 minutes to fix.

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 13:00):

I wonder now if the whole duplication effort was really worth, but well, that's what we have now.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:01):

Guillaume Melquiond said:

For the user? None.

That made me think that it doesn't qualify for the "Major enhancements section". But again, how about a "Major changes" section?

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 13:01):

Sure.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:01):

Théo Zimmermann said:

I wonder now if the whole duplication effort was really worth, but well, that's what we have now.

Well I couldn't have delivered CompCert and VST without it.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:03):

And anyway, I also did this as blueprint for handling such situations. The current solution looks trivial, but it actually took a bit of discussion.

view this post on Zulip Théo Zimmermann (Apr 21 2022 at 13:03):

Let me know when to send the announcement (I expect you want to update the GitHub release notes first).

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:03):

OK, I will add a "Major changes" section. I will do this now.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:10):

I added a "major changes" section and clarified the future plans in the detailed notes on Flocq.

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:10):

@Théo Zimmermann : is there a version specific link to the Coq changes - I can only find (https://coq.inria.fr/refman/changes.html) which I guess will change over time.

view this post on Zulip Karl Palmskog (Apr 21 2022 at 13:12):

one small proposed change:

coq-flocq has been updated to version 4.0.0, which is (slightly) incompatible with Flocq 3. Since coq-vst and coq-compcert have not yet fully switched to Flocq 4, Flocq 3 is included as a separate package - see the notes below for details.

view this post on Zulip Pierre Roux (Apr 21 2022 at 13:13):

Michael Soegtrop said:

Théo Zimmermann : is there a version specific link to the Coq changes - I can only find (https://coq.inria.fr/refman/changes.html) which I guess will change over time.

Maybe https://coq.inria.fr/refman/changes.html#version-8-15 (the sections seem to stack up in changes, so this should remain)

view this post on Zulip Michael Soegtrop (Apr 21 2022 at 13:18):

@Karl Palmskog @Pierre Roux : thanks, I did the changes.

@Théo Zimmermann : should be good to go.


Last updated: Jan 29 2023 at 19:02 UTC