Stream: Coq Platform devs & users

Topic: Coq 8.15


view this post on Zulip Michael Soegtrop (Jan 18 2022 at 16:52):

@Karl Palmskog : I just did a first pick for 8.15. There are 6 opam packages which restrict Coq to 8.14, but compile fine with 8.15. Should I push the relaxed opam packages or inform the maintainers? All in one PR or separate PRs?

Search for works with 8.14 version patchin 8.15 pick to see which packages are affected.

view this post on Zulip Karl Palmskog (Jan 18 2022 at 17:55):

@Michael Soegtrop if we want to really ensure the packages work with 8.15, then easiest if you submit PRs with of 3-4 packages each, so CI doesn't time out.

But if there are packages you don't feel even need testing with the opam archive CI on 8.15, you can put them in one large PR and use the ci-skip command, like Guillaume does here: https://github.com/coq/opam-coq-archive/pull/2043

view this post on Zulip Michael Soegtrop (Jan 19 2022 at 14:30):

I like CI, so I will split it into smaller PRs (or even make individual ones - maybe I create a script for this).

view this post on Zulip Michael Soegtrop (Jan 20 2022 at 10:53):

@Gaëtan Gilbert : just wanted to let you know that things are going reasonably well and that we most likely will have a Coq Platform preview which at least covers the "classic" Coq Platform content with proper releases early next week.

view this post on Zulip Michael Soegtrop (Jan 23 2022 at 19:14):

The main branch is pretty close to what I want to release on Tuesday. I just want to have a look at the two ToDo topics in (https://github.com/coq/platform/issues/139), that is the quickchick Windows issue and the Ubuntu CoqIDE icon issue. Then there might be a few last 8.15 packages (stdpp and iris just came in - not yet done).

So it would make sense to review the main branch.

view this post on Zulip Michael Soegtrop (Jan 24 2022 at 11:13):

Meanwhile stdpp, iris and coq-hammer for 8.15 came in, so the last package which does not have a release which compiles for 8.15 is mathcomp-analysis. This a very good yield for one week!

The issue with OCaml on Ubuntu 21 also seems to have been solved in the last days - still need to test it.

So all which remains are a few minor issues, e.g. the icon package for CoqIDE on Ubuntu is not complete.

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

This a very good yield for one week!

And this was without even putting a strong focus on the date of the preview release in the notification issues.

view this post on Zulip Michael Soegtrop (Jan 24 2022 at 13:21):

Indeed. Thinking about what months long mess it has been with 1/3 of the packages to get something patched together with a lot of duct tape in the old Windows installer days, I am very pleased. But of course this is to a good part also due to the improved Coq CI.

view this post on Zulip Karl Palmskog (Jan 24 2022 at 13:26):

I don't think we should underestimate the social aspects here, as in, the incentives of being part of the Coq platform

view this post on Zulip Karl Palmskog (Jan 24 2022 at 13:28):

and once the incentives are in place, I think a lot of work can become routine


Last updated: Jan 30 2023 at 12:03 UTC