Michael Soegtrop (Jan 16 2023 at 14:03): Michael Soegtrop (Jan 16 2023 at 14:03):I just released Coq Platform 2022.09.1 (with Coq 8.16.1). Sorry that it took so long - I had severe problems with CI each week breaking another platform.
@Théo Zimmermann, @Enrico Tassi, @Karl Palmskog : would you please go over the release notes?
Who does the announcement?
Théo Zimmermann (Jan 16 2023 at 14:04):Glad to hear! I was about to ask how the release was going and if it was relevant to add a preview version with Coq 8.17 (given that there are already a bunch of compatible packages), but too late for that, I guess ;-D
Théo Zimmermann (Jan 16 2023 at 14:05):I will review the release notes, and I can take care of sending the announcement as usual.
Théo Zimmermann (Jan 16 2023 at 14:06):Oh wow, there's an ARM macOS installer now!
Théo Zimmermann (Jan 16 2023 at 14:10):I think you should remove "There are two patches to CoqIDE included, which are not in the 8.16.0 release", since this release is based on 8.16.1 now.
Théo Zimmermann (Jan 16 2023 at 14:16):There's also a missing backtick in The `COQLIB environment variable is not used.
Théo Zimmermann (Jan 16 2023 at 14:16):I can fix both of these issues if you want.
Théo Zimmermann (Jan 16 2023 at 14:16):Ah, and the installer section still says "Binary installers are provided for the 2022.09~beta1 pick of Coq 8.16.0".
Théo Zimmermann (Jan 16 2023 at 14:18):Last remark: do you want to inform the users that this will be the last release where 32 bit installers for Windows are made available?
Théo Zimmermann (Jan 16 2023 at 14:22):@Michael Soegtrop Let me know if you want me to do the fixes to my three first remarks.
Michael Soegtrop (Jan 16 2023 at 14:23):@Théo Zimmermann : yes please go ahead and do the changes you mentioned above.
Michael Soegtrop (Jan 16 2023 at 14:25):Regarding 32 bit Windows: There is an official archive for 32 bit cygwin now and official instructions on how to install it and I adjusted the Ci accordingly. So theoretically one could build it like this until it finally breaks. There might be security issues in libraries, though after a while.
IMHO we should do one more release and then just keep the option to build it from sources.
Karl Palmskog (Jan 16 2023 at 14:29):@Michael Soegtrop do you have a specific link for the release notes? If it's in a PR I can make inline comments.
Michael Soegtrop (Jan 16 2023 at 14:30):@Karl Palmskog : the release notes are the notes for the release found here (https://github.com/coq/platform/releases).
Michael Soegtrop (Jan 16 2023 at 14:36):One more note on 32 bit: one could also patch up the MinGW32 toolchain on 64 bit cygwin. Building for 32 bit MinGW on 64 bit cygwin is not much more cross than building for 32 bit MinGW on 64 bit cygwin, except that Windows apparently has a file system hack so that it depends on the 32/64 bit of the executable reading a DLL if it will see a 32 bit or 64 bit version of the DLL. This messes up linking - at least this was so last time I tried it. One can fix this y copying the 32 bit files with a 32 bit copy program and direct the linker there. One would then need this 32 bit copy program as binary download (since one can't build it without itself). It is a bit messy, but probably less messy than 32 bit cygwin.
Karl Palmskog (Jan 16 2023 at 14:36):quick comments:
Michael Soegtrop (Jan 16 2023 at 14:37):Or we just drop 32 bit after the next release and are done with it.
Michael Soegtrop (Jan 16 2023 at 14:43):@Karl Palmskog : I implemented your changes - can you please double check.
Michael Soegtrop (Jan 16 2023 at 14:45):Regarding the sertop issue: I discussed this with @Emilio Jesús Gallego Arias - afair he said it would be a larger task to unify the startup code of coq tools and sertop, but he intends to do it. Indeed I didn't create an issue for it.
Karl Palmskog (Jan 16 2023 at 14:47):looks good, final thing is that maybe I would add a link to OCamlfind:
From Coq 8.16.0 on, Coq uses Ocamlfind to find shared libraries used by Coq tools and plugins.
Théo Zimmermann (Jan 16 2023 at 14:48):Michael Soegtrop said:
Or we just drop 32 bit after the next release and are done with it.
Yes, that would probably be the best move it if requires non-negligible work.
Michael Soegtrop (Jan 16 2023 at 14:51):The snap landing page also updated (and I updated the Readme). So all is fine :-)
Théo Zimmermann (Jan 16 2023 at 15:01):Announcement proposal:
Subject: Coq Platform 2022.09.1 release with Coq 8.16.1
Body:
Dear Coq community,
On behalf of the Coq development team, the release manager of Coq 8.16, and the Coq Platform team, we are happy to announce the immediate availability of the Coq Platform 2022.09.1 release.
Release highlights:
The latest version of Coq has been updated to 8.16.1, which fixes critical soundness bugs with previous versions, and brings other improvements.
Many new packages have been added. In particular, Itauto, mathcomp-algebra-tactics and mathcomp-word join the "full" level, and MetaCoq, Bedrock2 and Fiat-crypto join the "extended" level. See https://github.com/coq/platform/releases/tag/2022.09.1 for the complete list of additions.
This is the first Coq Platform release which contains a MacOS "M1 / M2 / Apple silicon / ARM" DMG installer.
The main supported version is Coq 8.16.1.
Several compatibility versions with Coq 8.12 to 8.15 are available, including one for Coq 8.15 with a package collection that tries to be as similar as possible to the Coq 8.16.1 pick.
Installers for Coq 8.16 and Coq 8.15 with the newest package collection are available for Windows, macOS, and Linux (Snap).
You can also install the Coq Platform using opam-based scripts, which give you access to the main supported version, as well as any of the many compatibility versions.
To learn about the Coq Platform and get access to the installers, please refer to: https://github.com/coq/platform/releases/tag/2022.09.1
Karl Palmskog (Jan 16 2023 at 15:03):maybe:
The latest version of Coq has been updated to 8.16.1, which fixes critical bugs with 8.16.0.
We did have soundness bugs, right?
Théo Zimmermann (Jan 16 2023 at 15:03):Yes
Théo Zimmermann (Jan 16 2023 at 15:04):But I was ambiguous on purpose on the version from which we are updating, since the previous release with 8.16.0 was a beta release.
Théo Zimmermann (Jan 16 2023 at 15:04):And I repeated the new package list from the beta announcement.
Michael Soegtrop (Jan 16 2023 at 17:53):@Théo Zimmermann : thanks, the announcement sounds good to me. I don't think it is necessary to mention the soudness bugs since there was no non beta Coq Platform release of 8.16.0. It might make sense to mention the M1/M2 Apple DMG installer - it was quite a bit if work and probably affects a lot of people meanwhile.
Michael Soegtrop (Jan 16 2023 at 17:54):@Maxime Dénès : talking of M1/M2: I lost track of the INRIA rented M1 runner. It is up and running?
Théo Zimmermann (Jan 16 2023 at 20:32):It might make sense to mention the M1/M2 Apple DMG installer - it was quite a bit if work and probably affects a lot of people meanwhile.
Right, I intended to but forgot. I'll add this and post tomorrow.
Karl Palmskog (Jan 16 2023 at 20:33):Maybe:
The latest version of Coq has been updated to 8.16.1, which fixes critical soundness bugs with previous versions.
I think we can remind people that if you take soundness seriously, latest minor version is the way to go.
Karl Palmskog (Jan 16 2023 at 20:58):I think we need to update the text on the Snap page: https://snapcraft.io/coq-prover
This snap contains the Coq prover version 8.15.1 along with CoqIDE and number of Coq plugins and libraries. Please refer to
https://github.com/coq/platform/blob/main/doc/README%7E8.15%7E2022.04.md
This should be:
This snap contains the Coq prover version 8.16.1 along with CoqIDE and number of Coq plugins and libraries. Please refer to
https://github.com/coq/platform/blob/main/doc/README%7E8.16%7E2022.09.md
Théo Zimmermann (Jan 16 2023 at 20:58):Karl Palmskog said:
Maybe:
The latest version of Coq has been updated to 8.16.1, which fixes critical soundness bugs with previous versions.
I think we can remind people that if you take soundness seriously, latest minor version is the way to go.
OK. Especially relevant since the soundness issues were already there in Coq 8.15.
Karl Palmskog (Jan 16 2023 at 21:04):to me at least, Fiat-crypto in particular is a nice feat of release engineering (this was something that was quite difficult to get up and running before the Platform). We might considering highlighting it:
Fiat-crypto can generate correct-by-construction code in C for cryptographic primitives.
Maxime Dénès (Jan 16 2023 at 22:26):@Michael Soegtrop yes, the M1 runner is up and running. Sorry for not having found the time to communicate more about it. We can discuss soon what you need me to set up (early february)
Michael Soegtrop (Jan 17 2023 at 08:15):@Karl Palmskog : indeed the snap text is wrong - I thought it was automatically created by the snap script and automatically updated when the latest snap is updated, but apparently something went wrong - let me check.
@Enrico Tassi : is the text on the snap landing page auto updated with the description of the latest snap?
Michael Soegtrop (Jan 17 2023 at 08:25):@Karl Palmskog @Enrico Tassi : apparently it is not auto updated, so I changed it and added an item to my release process notes.
Michael Soegtrop (Jan 17 2023 at 09:00):Apparently there is an issue with the MacOS signatures - the signatures are there but my Mac doesn't seem to accept them. Can someone with a Mac please test the installers? It did work for me before.
Michael Soegtrop (Jan 17 2023 at 09:12):Not sure what it was - now on right clock open it does show again the "open" option (it still shows an error message because it is signed but not notarised).
Michael Soegtrop (Jan 17 2023 at 09:31):@Maxime Dénès : please ping me when you have time - we should enable this in February, so that it works for the 2023.03 release.
Théo Zimmermann (Jan 17 2023 at 10:08):Michael Soegtrop said:
apparently it is not auto updated, so I changed it and added an item to my release process notes.
By any chance, are these release process notes public or could they be made public (in the platform repo or the wiki)? It would be helpful to have them public to be able to request volunteer help more easily in the future.
Michael Soegtrop (Jan 17 2023 at 10:15):@Théo Zimmermann : I can clean them up and publish them in the maintainer docs folder of the repo.
Karl Palmskog (Jan 17 2023 at 23:10):pitch for a @CoqLang tweet:
Check out the new Coq Platform 2022.09.1 release with Coq 8.16.1, which includes many bugfixes and several new packages like MetaCoq and Fiat-crypto! Besides opam-based installation scripts, this release has convenient binary installers for Windows, Linux (Snap), and macOS on both Intel and Apple silicon: https://github.com/coq/platform/releases/tag/2022.09.1
Michael Soegtrop (Jan 18 2023 at 08:14):@Karl Palmskog : thanks looks good!
Théo Zimmermann (Jan 18 2023 at 09:58):This is too long for Twitter by 50 characters.
Karl Palmskog (Jan 18 2023 at 10:03):OK, shorter version:
The Coq Platform 2022.09.1 release with Coq 8.16.1 is out, including new packages like MetaCoq and Fiat-crypto! Besides opam-based installation scripts, there are binary installers for Windows, Linux (Snap), and macOS on both Intel and Apple silicon: https://github.com/coq/platform/releases/tag/2022.09.1
Karl Palmskog (Jan 18 2023 at 10:04):(this is like that exercise I recommend to students, pitch your research in 25, 50, 100,500 words)
Théo Zimmermann (Jan 18 2023 at 10:08):Maybe nowadays they will just write the long version and ask ChatGPT to shorten it :laughing:
Théo Zimmermann (Jan 18 2023 at 10:10):Sent
Last updated: Jun 03 2023 at 03:01 UTC