Stream: Coq Platform devs & users

Topic: Coq Platform 2021.07


view this post on Zulip Michael Soegtrop (Jun 13 2021 at 10:18):

I started to work in the 2021.08 release.

@Enrico Tassi : one thing I am unsure about is how we do the branch naming. Since coq.dev stopped working just when I was ready with my integration of different Coq versions into one Coq Platform release and I was busy after that, it never made it into the 2021.02 branch. So I am unsure if I should merge it there? But I guess the plan is anyway to rename it back to master after it is merged with the dev branch?

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:39):

Great! I think we should pospone to switch to a single branch after 2021.08 is out

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:40):

I'll try to help a little next week, maybe we can coordinate on monday

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:40):

So do you suggest that I simply push the multi version stuff as new 2021.08 branch?

Btw.: 2021.08 or 2021.07?

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:44):

Thinking about it a bit more: It might make sense to keep separate branches, because it might make sense that a Coq 8.13 installed with 2021.08 has newer packages than a Coq 8.13 installed with 2021.02. Not sure about this, though.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:44):

I'm a bit outdated, I did not follow much in the last month or so. I'm not so sure my judgement can help. IIRC #102 was ok, but i'm not sure I would touch 2021.02, since that one is supposed to be stable

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:45):

ideally #102 should go to master, as we should fork off 2021.08 at some point, but I'm not sure either

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:45):

Well my changes don't change the outcome - they just also allow to install Coq 8.12 and Coq dev. For Coq 8.13 the result is the same, except for the opam switch name.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:46):

Well right now we don't have a master branch.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:46):

Maybe @Théo Zimmermann has ideas as well.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:47):

if the outcome is unchanged, then merging is safe... my main problem is that I don't know where to push fixes. For example the snap one I've just merged, I pushed it to .02, but I hope it also goes in .08

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:47):

The question is if we should have one master branch from which we tag all releases or not. This would be possible if we say that the package pick for 8.13 is constant for all times. If we have separate branches, we could have different package picks for 8.13 in 2021.02 and 2021.08.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:47):

in Coq all fixes go to master, then we may push them to the other branches if we want

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:48):

In any case I will rebase to latest 2021.02 before I branch off 2021.08.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:48):

Michael Soegtrop said:

The question is if we should have one master branch from which we tag all releases or not. This would be possible if we say that the package pick for 8.13 is constant for all times.

This option seems the best to me

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:49):

(once #102 is merged)

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:49):

So you say that the package pick for Coq 8.13 should never be touched.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:50):

I'm not su sure I understand this constraint.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:50):

I think this is OK. and it might be more confusing than helpful to have separate picks for the same version of Coq in 2021.02 and 2021.08. Of cause this would also be more maintenance effort.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:51):

Well we said that for one Coq Platform the package pick shall never be changed except for critical bug fixes.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:52):

The question is if we could have a Coq Platform 2021.02-8.13 and 2021-08-8.13 with different picks, say VST 2.8 instead of VST 2.7.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:52):

If we do this, we need different branches to handle it technically.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:53):

Hum, because you want to be able to release fixes for 2021.02-8.13?

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:54):

Not fixes - fixes could go into 2021.02.X (of cause for this one also needs a branch ...).

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:54):

yes, that is what I meant

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:54):

The idea is more to have updated 8.13 compatible packages. Like VST 2.8 and CompCert 3.9 all work for 8.13 and 8.14.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:55):

In 2021.02 we have VST 2.7 and CompCert 3.8.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:55):

imo 2021-08-8.13 should have 2.8+3.9, while 2021.02-8.13 stays with 2.7+3.8

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:56):

if we need to branch for this, we will, but isn't just about having multiple pick (not per Coq version, but per pair platform-coq)?

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:56):

OK, I agree with that. Then we definitely need long term separate branches for each release and not just one master branch from which we do tags.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:57):

I guess we went through this discussion already ...

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:57):

Sorry, I told you I'm a bit off ;-)

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:58):

No, I meant I turn mentally in circles sometimes.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 12:59):

So I push the multi Coq thing as master (it is already rebased to 2021.02), then I fix everything (dev has issues) and then I branch of 2021.08 from master?

view this post on Zulip Enrico Tassi (Jun 13 2021 at 12:59):

that would be ok.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:00):

I still wonder if "branch of 2021.08 from master" is really needed after 102

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:00):

Hmm - I don't understand your last comment.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:01):

I did not look at the code, but I can imagine it being about adding a file coq_package_2021.08_8.14

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:02):

102 adds support for coq_packages_8.x IIRC

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:02):

Ah, you mean we can branch off 2021.08 later - more before we do 2122.02?

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:02):

I was stretching the idea to have one package selection file per platform times coq versionm eg coq_packages_2021.02_8.13

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:04):

yes. I'll try to clarify:

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:07):

I guess master will select a default package selection.

If it is dev, then we are forced to branch, change the default selection, and then tag at release time.

If the default selection is the latest released platform, then we don't really need to branch when we tag.
Unless we need to do a point release for an old platform (and then we would branch just to change the default selection I guess).

Ideally all the "stuff" is in master, and we only select which one the user gets by default.

Am I dreaming?

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:10):

The multi-version thing is here (https://github.com/MSoegtropIMC/platform/tree/multi-version)

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:11):

You have several package list files in (https://github.com/MSoegtropIMC/platform/tree/multi-version/versions) and can choose via command line or interactively one of these.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:11):

The idea for CI is to run all of them (at least sometimes) as a matrix.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:13):

Yes, I was wondering if it is possible to have ./coq_platform_make.sh -packages=2021.02_8.13 and, at the same time, ./coq_platform_make.sh -packages=2021.08_8.13 (I know that branch/PR only lets you ./coq_platform_make.sh -packages=8.13)?

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:13):

So yes, we can tag releases from master and only branch of release branches in case there is a real need - as you say a patch release after a new version has been released. I would say we can wait until this happens.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:14):

So CI/matrix can test multiple coq/platform combinations, all in the master branch

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:14):

ok

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:14):

It can do 8.12 + 8.13 + dev, but as is not 2021.02-8.13 and 2021.08-8.13, although this would be easy to add.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:15):

if we add it, then I think branch are way less nedded (which is good, IMO)

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:15):

Maybe it would be less confusing to users if we would actually offer "8.13 (2021.02 pick)" to the user in 2021.08.

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:16):

Then we could of cause also test it in CI and also do patches to this package list (the 2021.02 8.13) from master.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:16):

indeed

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:17):

so 2021.08 will include a bunch of possible selections, even the old 2021.02

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:17):

So the user would get a list like

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:18):

At some point one could only show a selection interactively, but still have them all.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:18):

yes. If we do so, there will be no need to tag a fix 2021.02.2, for exammple, we can just release a 2021.08.2 with an updated selection for the old platform.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:19):

(I'm trying to see all scenarios)

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:19):

Yes. And as I said, it is likely less confusing than telling users to use Coq 8.13 from Coq Platform 2021.02 or 2021.08.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:19):

we agree

view this post on Zulip Enrico Tassi (Jun 13 2021 at 13:20):

gotta go now, ciao

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:20):

Perfect. Also this has the advantage that one doesn't have to know if one should name it 2021.07 or 2021.08 before one actually does the release ;-)

view this post on Zulip Michael Soegtrop (Jun 13 2021 at 13:20):

Ciao, thanks for the helpful discussion!

view this post on Zulip Théo Zimmermann (Jun 13 2021 at 20:40):

I've read the discussion only now but I fully agree with your conclusion.

view this post on Zulip Andrew Appel (Jul 28 2021 at 19:54):

I also just skimmed the end of the discussion, this makes sense to me. I look forward to the release of "Coq 8.13 (2021.08 package pick)" without having to wait for Coq 8.14.

view this post on Zulip Théo Zimmermann (Jul 29 2021 at 09:37):

Yeah, given the delays in getting 8.14 out, this would definitely make sense.

view this post on Zulip Michael Soegtrop (Aug 18 2021 at 08:23):

@Théo Zimmermann @Guillaume Melquiond : is there news on the 8.14 release? I was super busy the last few weeks but it is getting better.

view this post on Zulip Ali Caglayan (Aug 18 2021 at 08:59):

We still have some blockers on the release that need to get resolved

view this post on Zulip Ali Caglayan (Aug 18 2021 at 08:59):

https://github.com/coq/coq/milestone/32

view this post on Zulip Ali Caglayan (Aug 18 2021 at 08:59):

They are some real head scratchers unfortunately.

view this post on Zulip Michael Soegtrop (Aug 19 2021 at 17:00):

Is there an estimation? I don't want to push - I just need to make sure that I have a bit of time to do the platform work, and if it would take too long, I might do a 2021.08 pre release - either with 8.13 or with a 8.14 preview.

view this post on Zulip Théo Zimmermann (Aug 20 2021 at 15:00):

Hi @Michael Soegtrop! I personally think that the 8.14 release has already been delayed way too much and maybe we should consider filling @Andrew Appel's request of a 2021.08 platform release / package pick, without waiting for Coq 8.14.

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

@Théo Zimmermann : OK, I will look into it. What version of Coq would you recommend? 8.13 or should we do some sort of 8.14 preview tag?

view this post on Zulip Théo Zimmermann (Aug 21 2021 at 17:18):

Yes, 8.13 could be the main version. Ideally we would also include an 8.14 preview tag, but that would require the involvement of @Guillaume Melquiond to make a tag.

view this post on Zulip Michael Soegtrop (Aug 21 2021 at 17:56):

I guess the 8.13/8.14 question also depends on what desirable versions of packages require - if everything runs nicely with 8.13, I think we should make a clean 8.13 version and if 8.14 is ready, we can do another release. If we have 2021.08 and 2021.09 then, so be it.

view this post on Zulip Michael Soegtrop (Aug 21 2021 at 17:56):

I will prepare everything during this week.


Last updated: Nov 29 2023 at 04:01 UTC