Stream: Coq Platform devs & users

Topic: New Coq Platform master branch


view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:23):

@Théo Zimmermann @Enrico Tassi : I am unsure how to handle the 2021.09 "multi version" branch. It is operational, but currently lives in my fork. Do you think it is time to switch the Coq Platform master branch to 2021.09 and maybe do a tag "2021.09~pick2021.02"? I am afraid that this might confuse people but then I can't work on adding packages on the old branch.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:24):

I don't understand what you propose exactly.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:28):

Currently the master branch of Coq Platform is 2021.02. At some point we have to switch to 2021.09. I am unsure what the best moment for switching is - when everything is ready (including new packages) or when we start to work on it with a wider audience (integration of new packages).

The main new thing (currently) in 2021.09 is that it supports multiple package lists, e.g. for different Coq versions. The main rationale behind this is that we don't want to technically support old versions of the platform forever (the adjustments to OS changes are a bit of work). So 2021.09 allows to build various versions of Coq with a common script base.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:29):

OK, now I get it. You're confusing "master branch" and "default branch on GitHub".

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:29):

Possibly ...

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:30):

"master branch" means a branch called "master". There is no "master" branch in the platform repository at the current time.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:30):

There is one branch on which the daily CI runs and which the user sees when visiting the page.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:30):

Yeah, that's called the "default branch".

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:30):

The current default branch is 2021.02. It was expected that at some point we would switch the default branch to 2021.09.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:31):

Yes. The question is when.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:31):

Yesterday I did a release of 2021.02 - so today might be a good time.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:31):

That's not the only question though. Does it make sense to keep creating branches after platform releases if we have a multi-version model now?

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:31):

IMHO it doesn't.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:32):

I think the new default branch should just be called "master" or "main".

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:32):

That is another question - possibly not. One can think about changing the pick also for older Coq versions, though. But the the multi version branch could support multiple picks for each Coq version ...

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:33):

It might be less confusing then, yes.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:33):

Yes, I thought this would be the case (that the multi-version branch would support both installing various versions of Coq at various package picks).

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:35):

So the conclusion is that I push my fork's 2021.09 to the main fork as master branch and make this the default branch? Or do we wait with the default branch switch a bit?

view this post on Zulip Enrico Tassi (Sep 21 2021 at 07:41):

IMO the question is: how much free time do we have right now? (I'm a bit busy for example).
If there is energy, I'd switch to the new model now, just have the master (actually "main" is the new religion) branch with all platform versions in it and make a tag when the the package selection for 2021.09.0 is ready.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:43):

Do you think I should also make a tag of the multi version branch with the 2021.02 package selection?

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 07:46):

Not necessarily useful if the 2021.02 package selection keeps being supported.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:47):

@Enrico Tassi : I also don't have that much time, but I there is not much choice - we need to keep things going.

view this post on Zulip Enrico Tassi (Sep 21 2021 at 07:49):

I mentioned the time argument because "new thing -> new problems", but if you say it works I guess I'm just worrying for nothing.

view this post on Zulip Enrico Tassi (Sep 21 2021 at 07:49):

BTW, I did write a script in the past to notify upstream authors of an upcoming release

view this post on Zulip Enrico Tassi (Sep 21 2021 at 07:50):

It's probably broken now, but maybe I can repair it.

view this post on Zulip Enrico Tassi (Sep 21 2021 at 07:51):

Indeed, it is based on Coq's CI rather than a package pick from the platform, see dev/tools/notify-upstream-pins.sh

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 07:55):

I need to cherry pick the latest changes on 2021.02, but otherwise it works. The only changes are the multi version stuff and a switch to OCaml 4.10.

I guess in the main Readme, we should have a note that people should use tagged releases.

view this post on Zulip Enrico Tassi (Sep 21 2021 at 08:00):

The script basically works, it just lacks the list of packages actually part of the platform.
It prints a bunch of URLs you can click to open an issue with a prefilled message.

view this post on Zulip Enrico Tassi (Sep 21 2021 at 08:01):

eg click this (please don't finalize the issue)

view this post on Zulip Enrico Tassi (Sep 21 2021 at 08:03):

The only thing I had to do is to checkout v8.14, then:

and I got a bunch of urls like that one. One would need to filter out project irrelevant to the platform and adjust the message.

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

@Enrico Tassi : thanks, I will have a look after lunch - I guess you don't mind if I put an adjusted copy into Coq Platform.

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

I guess in the main Readme, we should have a note that people should use tagged releases.

Why should they? What advantage does it procure? It seemed to me that using the latest version of the main branch should be always preferred since it may contain various fixes.

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

It is a bit tricky to ensure stability when we add a larger number of packages and change the picks, since it has quite a number of combinations. I think we can control this reasonably well but I am not sure.

view this post on Zulip Enrico Tassi (Sep 21 2021 at 08:19):

I guess it is like using (branch) v8.13 rather than (tag) V8.13.2 ... I'd recommend the latter to the random user

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 08:22):

Sure, but nothing forces us to merge this changes into master / main until they are not finalized. We could follow the model of Docker-Coq-Action, where there is a branch which users can follow (v1) and a branch which is used to develop new features (it is called master in this case, but a common name for this use is to call it dev).

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 08:23):

My point being that if hot fixes are merged, there is no reason not to make them available right away...

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 09:25):

The issue is that github can run daily CI only on the default branch (without a lot of hacks at least) and I need to run daily CI on the branch which is actively developed, so this needs to be the default branch.

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 09:32):

Good point on the daily CI. Two (three) solutions:

  1. I have gained experience on GitHub workflows lately and testing another branch may be as easy as changing an argument to the actions/checkout@v2 step (except that statuses may be reported back to the wrong commit)...
  2. The version in-development could very well be continuously pushed to the default branch but hidden being a specific option, so that users do not see it even if they use the latest commit on the branch.
  3. We could indeed encourage users to rely on tagged versions, but it seems likely that some of them will disregard this recommendation (because people often read the doc too fast) and will clone the platform repository without checking out a tag.

view this post on Zulip Michael Soegtrop (Sep 21 2021 at 10:58):

I don't want to have the CI more complicated than necessary, so that contributors can understand it.

Another through: initially the daily CI is not important, since we anyway expect at least a build a day. If the changes becomes substantially less than one a day, it might be time to change. So I will make the 2021.09 branch the new main branch, but won't make it the default branch yet.

view this post on Zulip Michael Soegtrop (Sep 22 2021 at 07:23):

@Théo Zimmermann, @Enrico Tassi : I just wanted to let you know that I pushed my 2021.09 branch as main on coq/platform. As discussed I won't make it default for a while.

view this post on Zulip Michael Soegtrop (Sep 22 2021 at 12:35):

@Enrico Tassi : I added a version of your script adjusted to Coq Platform to PR https://github.com/coq/platform/pull/138. Can you please leave a comment there that you agree with the change of copyright?

Besides using the Coq Platform package list (from a specified package list file) I added a dump of all tags for each package, so that one can immediately check if there might be a suitable tag (or a newer tag than in CI). With a few lines more one can probably detect all used version schemes and automate this even further.

Thanks for the script - very useful!

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:39):

LGTM

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:42):

One note. If you CC a github issue, then GH displays (on that issue) the list of linked issues and they become red/green when they are close/open. So at a glance you see who did tag. My problem was that some people tag without writing a message, so you may not notice they did it, and looking at one issue is faster than looking at 20.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:43):

see the bottom of https://github.com/coq/coq/issues/12334 for a reference

view this post on Zulip Michael Soegtrop (Sep 22 2021 at 12:50):

Ah OK - thanks for the hint. I will then create a Coq Platform issue and reference it there.

view this post on Zulip Michael Soegtrop (Sep 22 2021 at 15:49):

@Enrico Tassi : I created the tracker (https://github.com/coq/platform/issues/139) and the upstream issues.

Do you think we also should have another script which creates info issues for all those where the latest tag does work - just to inform them about the timeline to give them a chance to do an update in a timely fashion?

view this post on Zulip Théo Zimmermann (Sep 22 2021 at 18:37):

Yes, I think so. Upstream maintainers should be notified of which version we intend to package and get a chance to correct that.

view this post on Zulip Michael Soegtrop (Sep 22 2021 at 21:11):

@Théo Zimmermann : OK, I will do so tomorrow. I just pushed to main a first version for 8.14, with those packages which do compile (the majority).


Last updated: Jan 30 2023 at 12:03 UTC