Stream: Coq Platform devs & users

Topic: Time to announce 2021.09


view this post on Zulip Michael Soegtrop (Nov 06 2021 at 20:10):

@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.

view this post on Zulip Karl Palmskog (Nov 07 2021 at 14:49):

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

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

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 07:49):

Here is a proposal:

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

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

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

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

view this post on Zulip Michael Soegtrop (Nov 08 2021 at 08:03):

Looks good thanks! I just would think about linking the 8.13 package list readme (https://github.com/coq/platform/blob/2021.09.0/doc/README_2021.09.0_8.13.md).

I will change the Release text to include the Ltac debugger doc as you did.

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

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

See the Plaform Charter for more on the Platform concept.

view this post on Zulip Karl Palmskog (Nov 08 2021 at 08:06):

one might even link to CEP 52, such as:

See the Plaform Charter for more on the Platform concept, and CEP 52 for how the Platform is integrated into [related to?] the Coq release cycle.

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

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

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

view this post on Zulip Michael Soegtrop (Nov 08 2021 at 08:11):

@Théo Zimmermann : OK, I will change the names.

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

view this post on Zulip Karl Palmskog (Nov 08 2021 at 08:14):

can do a PR if you like

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

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

view this post on Zulip Karl Palmskog (Nov 08 2021 at 08:15):

To learn more about the Coq platform, including how to use it:
https://github.com/coq/platform/blob/2021.09.0/README.md

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

view this post on Zulip Michael Soegtrop (Nov 08 2021 at 08:20):

@Karl Palmskog : https://github.com/coq/platform/blob/2021.09.0/README.md is a tag link.

view this post on Zulip Michael Soegtrop (Nov 08 2021 at 08:21):

Yes, the next one is planned this month.

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

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

view this post on Zulip Enrico Tassi (Nov 08 2021 at 08:53):

This "message" is there, if you read carefully, but not that explicit.

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

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

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

view this post on Zulip Michael Soegtrop (Nov 08 2021 at 09:51):

@Enrico Tassi : I made things more explicit in the Release text.

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:26):

Karl Palmskog said:

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

main
From now on, this is the only active branch.

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

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

view this post on Zulip Enrico Tassi (Nov 08 2021 at 10:41):

Awesome!

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

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:44):

I'd say it is a "distribution". Where do you see the word "system" being used?

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:45):

The only place where I can see it is in "system independent" in the README.

view this post on Zulip Karl Palmskog (Nov 08 2021 at 10:46):

ah, I think I misread "system" from another context

view this post on Zulip Karl Palmskog (Nov 08 2021 at 10:46):

OK, let's go with "distribution" then

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:46):

Probably there should be a hyphen between "system" and "independent" BTW.

view this post on Zulip Karl Palmskog (Nov 08 2021 at 10:59):

https://github.com/coq/platform/pull/169 - "system" is just too generic for me, I specialize to "operating system" but open to other suggestions

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 16:42):

If everything is in order, should we send the announcement now?

view this post on Zulip Michael Soegtrop (Nov 08 2021 at 16:54):

@Théo Zimmermann : yes please. The text you posted still looks good to me.

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 16:58):

OK, sent!

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 17:58):

I forgot to also do a tweet but someone took care of that and it got retweeted by @CoqLang already ;-)

view this post on Zulip Karl Palmskog (Nov 08 2021 at 20:32):

maybe someone can give the nice tweeter a pointer to our Zulip style guide topic: https://twitter.com/intoverflow/status/1457453655498522627

.@CoqLang fam: do you use a linter? Tell me more

- Tim Carstens (@intoverflow)

Last updated: Jan 29 2023 at 19:02 UTC