@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?
works with 8.14 version patchin 8.15 pick to see which packages are affected.
@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
I like CI, so I will split it into smaller PRs (or even make individual ones - maybe I create a script for this).
@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.
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.
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.
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.
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.
I don't think we should underestimate the social aspects here, as in, the incentives of being part of the Coq platform
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