Time to announce 2021.09 · Coq Platform devs & users

@Théo Zimmermann @Enrico Tassi : the 2021.09.0 release is done and it would be time to announce the release on Coq club. As usual I would prefer if someone from INRIA does this.

Karl Palmskog (Nov 07 2021 at 14:49):

please announce on Discourse as well (and please tweet on @CoqLang the Discourse link)

Enrico Tassi (Nov 07 2021 at 15:38):

I can do it tomorrow. But please prepare a paragraph with the news, I did not really follow this time.

Théo Zimmermann (Nov 08 2021 at 07:49):

Dear Coq community,

On behalf of the Coq development team, the release managers of
Coq 8.13 and Coq 8.14, and the Coq Platform team, we are happy to
announce the immediate availability of the Coq Platform version
2021.09.0.

This is the first Coq Platform release which includes several
versions of Coq. Furthermore, the included package set was
significantly extended since the 2021.02.2 release.

The main supported version is:

- Coq 8.13.2 with an extended package collection.

Furthermore, we include two compatibility versions (8.13.2 with
previous package set, 8.12.2) and two preview versions:

- Coq 8.14.0 (with a preliminary (beta) package collection - not
  all packages support Coq 8.14 yet).

- A preview of the (not yet released) interactive GUI Ltac
  debugger for CoqIDE, based on Coq 8.14.0. See documentation at:
  https://github.com/coq/coq/wiki/Ltac-Debugger-Preview

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

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

Théo Zimmermann (Nov 08 2021 at 07:50):

Sending via email to coq-club@inria.fr + coq+announcements@discoursemail.com should take care of both Coq-Club and Discourse.

Karl Palmskog (Nov 08 2021 at 07:51):

I suggest including a link to the Platform charter, since people may not be in the clear what the platform really is.

Théo Zimmermann (Nov 08 2021 at 07:56):

The README whose link is at the end of the announcement is a good place to start to read about the platform nowadays, and it links to the charter. What do you think of the new sentence introducing this link? Or do you still think that a direct link to the charter is in order? (Note that, while still being relevant, the charter is not the most up-to-date piece of doc of the platform at the moment.)

Michael Soegtrop (Nov 08 2021 at 08:03):

Théo Zimmermann (Nov 08 2021 at 08:04):

BTW @Michael Soegtrop I think the way the Windows installers are named is problematic for not including the platform version. If a user downloads the installer from this release but also add the one from the previous release, they cannot distinguish them. And there will be the same problem with the 2021.11 release for Coq 8.14.0. The macOS naming scheme is better from that point of view.

Karl Palmskog (Nov 08 2021 at 08:04):

I think the README charter link is a bit hidden in the prose. As usual one could break up the text with bullets:

The main goal of the Coq Platform is to provide a system for developing and teaching with Coq that is:

Karl Palmskog (Nov 08 2021 at 08:06):

Michael Soegtrop (Nov 08 2021 at 08:08):

@Théo Zimmermann : yes I have it on my ToDo list to have a more consistent naming of the installers. I kept the naming as is for the time being to make sure I don't get myself confused. But if you think it is an issue, I can change the names.

Théo Zimmermann (Nov 08 2021 at 08:10):

Yes, I think it needs to be changed for this release (even if the name scheme is not final) to avoid confusion with the installer from the previous release.

Michael Soegtrop (Nov 08 2021 at 08:10):

@Karl Palmskog : do you refer to the structure of the README.md file itself, or do you refer to the release announcement?

Michael Soegtrop (Nov 08 2021 at 08:11):

Karl Palmskog (Nov 08 2021 at 08:13):

@Michael Soegtrop I'm fine with changing only the README.md and not the announcement (with my proposed changes it should be a bit easier to find out "what is the platform" in the README text)

Karl Palmskog (Nov 08 2021 at 08:14):

Michael Soegtrop (Nov 08 2021 at 08:14):

So do you suggest that I change the tag the release points to (because the release points to the tagged Readme file)?

Karl Palmskog (Nov 08 2021 at 08:15):

fine with me to only change the README in the branch (I think that is linked to above?)

Karl Palmskog (Nov 08 2021 at 08:15):

Karl Palmskog (Nov 08 2021 at 08:19):

ah OK, so it's a tag. Well, fine with me if you don't want to change the tag this time, but I guess there will be more announcements.

Michael Soegtrop (Nov 08 2021 at 08:20):

Michael Soegtrop (Nov 08 2021 at 08:21):

Karl Palmskog (Nov 08 2021 at 08:26):

OK, so what branch do I submit PR against if I want README updated for next announcement?

Enrico Tassi (Nov 08 2021 at 08:52):

I think it should be made clear which is the "default pick", and list 8.14 as a preview of 2021.11.0 and 8.12 as a compat thingy.

Enrico Tassi (Nov 08 2021 at 08:53):

Enrico Tassi (Nov 08 2021 at 08:57):

Maybe you don't feel the same, so I'm not pushing this rephrasing if you don't like it. But to me this is a platform for 8.13 (the solid thing) plus a couple of previews (useful to test/port) and a legacy version (to ease porting forward old code). If we agree on this assessment, then I guess as a user I'd be happy to know how things are intended to be used.

Michael Soegtrop (Nov 08 2021 at 09:16):

@Enrico Tassi : yes this is the intention - I thought the ordering makes it clear. If you have ideas to improve the text, please let me know.

Enrico Tassi (Nov 08 2021 at 09:17):

I would just hoist the first item in the list, and then say something like "in addition to the main target, this P release also includes: - a preview of ... (sorry, I've to rush)

Michael Soegtrop (Nov 08 2021 at 09:51):

Théo Zimmermann (Nov 08 2021 at 10:26):

Théo Zimmermann (Nov 08 2021 at 10:39):

I've updated the announcement draft (above) to account for the changes that were discussed here.

Théo Zimmermann (Nov 08 2021 at 10:40):

In particular, given that now all the relevant links are on the release page, I've removed the link to the README from the announcement.

Enrico Tassi (Nov 08 2021 at 10:41):

Karl Palmskog (Nov 08 2021 at 10:43):

is the Platform a "system" or actually more of an "environment"? We usually call Coq itself a "system"

Théo Zimmermann (Nov 08 2021 at 10:44):

Théo Zimmermann (Nov 08 2021 at 10:45):

Karl Palmskog (Nov 08 2021 at 10:46):