Stream: Coq Platform devs & users

Topic: Naming of the next releases


view this post on Zulip Michael Soegtrop (Jan 20 2022 at 13:04):

Since I am quite late with the 2021.11 release (just busy + CoqHammer) I wonder how we should name things.

For the 8.15 release I expect much less issues because the infrastructure is done and I also won't add that many packages, so end of February is quite realistic. But then I also want to make a release next week.

Should we keep the 2021.11 name - I think quite a few people got it from the main branch already - and name the next one 2022.02?

view this post on Zulip Théo Zimmermann (Jan 20 2022 at 13:09):

As I've already expressed elsewhere (you know that already, but I will repeat it here), my suggestion is to name the one that will come next week 2022.01 to reflect the reality (and since the Snap track hasn't been requested yet---BTW, it should be done without waiting). This 2022.01 release would be the one which includes both Coq 8.14.1 (default package selection) and the beta Coq 8.15.0 selection. Naming it 2021.11 would be a bit weird given that 8.15.0 was not out by that date...

view this post on Zulip Michael Soegtrop (Jan 20 2022 at 13:41):

So do you suggest to have a 2022.01 and a 2022.02? Fine with me, I just think it might be slightly confusing as well.

Please note that we said that we could have minor releases which add new packages or picks to an existing Coq Platform release, so if I would have releases 2021.11 in time, then the 8.15 preview might have ended up in 2021.11.1, which then also brings 8.14.1.
The rule is that anything which exists should not change, except for highly compatible bug fixes.

view this post on Zulip Théo Zimmermann (Jan 20 2022 at 13:48):

So do you suggest to have a 2022.01 and a 2022.02? Fine with me, I just think it might be slightly confusing as well.

Yes, that's my suggestion. Although if you already expect 2022.02 to happen close to the end of February, it could also be renamed 2022.03 and planned for the first day of March.

Please note that we said that we could have minor releases which add new packages or picks to an existing Coq Platform release, so if I would have releases 2021.11 in time, then the 8.15 preview might have ended up in 2021.11.1, which then also brings 8.14.1.

Sure. But here, we do not have any preexisting 2021.11 release, so we are not bound by this.

view this post on Zulip Michael Soegtrop (Jan 20 2022 at 16:32):

OK, fine. I will go with 2022.01 and 2022.03 then.

@Enrico Tassi : can you please request the snap channel 2022.01?

view this post on Zulip Enrico Tassi (Jan 20 2022 at 17:37):

done: https://forum.snapcraft.io/t/2022-01-track-creation-for-coq-prover/28399

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

Are you taking care of answering to the points raised by roadmr?

view this post on Zulip Enrico Tassi (Jan 20 2022 at 18:39):

If you have the time, please go ahead.I guess the question are asked because we are requesting tracks more often than the initial 6 months

view this post on Zulip Enrico Tassi (Jan 20 2022 at 18:40):

Maybe @Michael Soegtrop can also reply with some info.

view this post on Zulip Théo Zimmermann (Jan 20 2022 at 19:01):

Are you responding right now? If yes, I'm happy to leave that to you, as I should get going soon.

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

I need to stop here, but I've a draft of an answer to the first point:

Hi,

  1. The Coq proof assistant is released every six months in theory, and the Coq Platform (which is released through Snap as coq-prover) mostly follows this cycle, but there was a long delay producing the 8.14 version of Coq, which resulted in a 2021.09 version which was still based on Coq 8.13 (but with major updates of other libraries). The 2022.01 version will be based on Coq 8.14, and we expect a 2022.03 to happen based on Coq 8.15 (which was released just four months after Coq 8.14 because a lot of changes had accumulated).

view this post on Zulip Théo Zimmermann (Jan 21 2022 at 09:24):

Sent a complete answer.

view this post on Zulip Enrico Tassi (Jan 21 2022 at 09:47):

A relly nice one, thanks

view this post on Zulip Michael Soegtrop (Jan 21 2022 at 10:59):

Regrading the snap team questions: I would just say that these are initial hick-ups. Coq Platform is really new which makes some things a bit hard to predict. We don't like to compromise on quality, so sometimes the timing suffers a bit.

view this post on Zulip Michael Soegtrop (Jan 21 2022 at 11:20):

@Théo Zimmermann : I just read your answer - really nice!

view this post on Zulip Théo Zimmermann (Jan 21 2022 at 11:21):

Thanks, feel free to add to it if you think it's useful.

view this post on Zulip Karl Palmskog (Jan 21 2022 at 11:22):

good answer. But in the future, I think we can be stronger about the 6-month cycle - it's not just an abstract/theoretical goal but an agreed-on aim that serves as a coordination mechanism for all the different stakeholders/participants

view this post on Zulip Théo Zimmermann (Jan 21 2022 at 11:24):

This makes sense. It would be really good to update our documentation to make this clearer.

view this post on Zulip Karl Palmskog (Jan 21 2022 at 11:27):

for example, a contributor to Coq itself is given a good estimate of when a PR to master makes it to release, which is critical, and people come around asking, where is 8.XY, when there is a delay.

view this post on Zulip Karl Palmskog (Jan 21 2022 at 11:29):

in my view, the only other related tool that has something similar is Isabelle, which I believe has committed to at least yearly releases. For Lean, there is as yet no official word on releases - this is the closest I have seen (bottom half of second picture): https://twitter.com/derKha/status/1471847464319729676

First novel (not previously published) content for my thesis whoo https://twitter.com/derKha/status/1471847464319729676/photo/1

- Sebastian Ullrich (@derKha)

Last updated: Jan 30 2023 at 11:03 UTC