Michael Soegtrop (Apr 05 2022 at 08:30): 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.
Julien Puydt (Apr 06 2022 at 05:20):I updated my comparison page to follow the corresponding csv description.
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)
Enrico Tassi (Apr 06 2022 at 14:57):Here: https://forum.snapcraft.io/t/2022-04-track-creation-for-coq-prover/29453
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.
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
Michael Soegtrop (Apr 11 2022 at 09:02):I will test and upload them later today.
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.
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.
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.
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?
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).
Théo Zimmermann (Apr 20 2022 at 17:47):I can take care of this tomorrow.
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:
Coq 8.15 is now stable and the default version proposed in the Coq Platform.
Flocq has been upgraded to major version 4.0.0. Flocq 3 is still available under the namespace Flocq3 because CompCert and VST depend on it. It is expected that the Flocq3 package will be removed when CompCert and VST become compatible with Flocq 4.
QuickChick has been re-enabled in compile-from-source mode on Windows
Several packages have been added: coq-ott and ott, coq-relation-algebra, coq-mathcomp-algebra-tactics, coq-extructures.
The main supported version is:
- Coq 8.15.1 with an extended and upgraded package collection.
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:
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.
Karl Palmskog (Apr 21 2022 at 12:27):you could mention Ott as well (but speaking in my own interest I guess)
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.
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
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".
Karl Palmskog (Apr 21 2022 at 12:29):was Gaëtan alone as RM of 8.15?
Théo Zimmermann (Apr 21 2022 at 12:29):I think so.
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.
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
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...
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.)
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
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
Karl Palmskog (Apr 21 2022 at 12:36):@Michael Soegtrop so do you think you will retire Flocq3 for 8.16.0 pick?
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.
Karl Palmskog (Apr 21 2022 at 12:37):sounds good to me, unless Michael has another proposal
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.
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.
Théo Zimmermann (Apr 21 2022 at 12:49):@Michael Soegtrop Do you agree with the current form of the release announcement proposal (above)?
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?)
Michael Soegtrop (Apr 21 2022 at 12:49):Yes. I will add a section "major version changes" under hightlights.
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).
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".
Michael Soegtrop (Apr 21 2022 at 12:53):(I know this is hard ...)
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?
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.Coreproved a close/far-path adder in Calc.Plus
made IEEE754.Binary a wrapper around IEEE754.BinarySingleNaN
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.
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.
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)
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.
Michael Soegtrop (Apr 21 2022 at 12:58):How about having a separate "Major changes" section?
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.
Michael Soegtrop (Apr 21 2022 at 12:59):@Guillaume Melquiond : could you describe in a few words, what the benefits of this change are?
Guillaume Melquiond (Apr 21 2022 at 12:59):For the user? None.
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.
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.
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?
Théo Zimmermann (Apr 21 2022 at 13:01):Sure.
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.
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.
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).
Michael Soegtrop (Apr 21 2022 at 13:03):OK, I will add a "Major changes" section. I will do this now.
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.
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.
Karl Palmskog (Apr 21 2022 at 13:12):one small proposed change:
coq-flocqhas been updated to version 4.0.0, which is (slightly) incompatible with Flocq 3. Sincecoq-vstandcoq-compcerthave not yet fully switched to Flocq 4, Flocq 3 is included as a separate package - see the notes below for details.
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)
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: Jun 03 2023 at 05:01 UTC