I plan to include a 8.16 preview "package pick" in the 2022.04.1 Coq Platform release (mostly done for Coq 8.15.2).
In a preview pick I usually just patch the opam packages in the Coq Platform local opam repo to allow the new Coq version and usually get pretty far with this, but for 8.16 the latest release of ssreflect does not compile. I would appreciate your opinion what I should do:
I don't think it makes any sense to publish a 8.16 preview without mathcomp.
Please do open the issues asking for 8.16-compatible releases on the package repositories (in general, not just for math-comp). If people happen to release new versions sufficiently fast, this means that you can include more tagged releases and fewer patched packages in the preview release.
I would anyway do this as part of the 8.16 preparations today. Here the situation is a bit special cause of the simultaneous release of 8.15.2 and 8.16+rc1.
If you think "wait two weeks" is the way to go, then I will do the 8.16 preparation now (which means creating all the issues).
Btw.: for 8.15+rc1 I got a fairly complete release (3 packages missing or so) within a day - I hoped it will be the same for 8.16+rc1 ...
@Théo Zimmermann : there is actually one problem with creating the "please tag" issues: in the past I always included the Coq Platform CI status of the latest release version of each package in the issue text. This doesn't make a lot of sense if mathcomp does not build.
I will see how far I get with the latest commit on master ...
If this does not work, I guess I will remove the CI information from the issue texts.
@Théo Zimmermann : I patched up a few mathcomp packages - I guess I need pin all to a master commit. So I will see what builds without mathcomp.
we currently don't have any effective way of testing packages with 8.16+rc1 in CI. I might do a release of aac-tactics nevertheless based on my local testing, but I think it would be good if we could get Docker images or similar out the door for 8.16+rc1 before we ask for releases.
I am not sure how well this will work - currently testing. That mathcomp does not build is an issue because a lot of packages depend on it. As it looks 8.16 deprecated a few things which break a lot of packages, but this might also be bad luck with the first few packages I tried. I am currently working on a package pick which simply disables everything which does not build (with just 8.16 enabled in the opam package).
Regarding Mathcomp, I added the subject for the next meeting next week: https://github.com/math-comp/math-comp/wiki#meetings
For other packages, I agree with Karl we should first get a Docker image of 8.16 to prepare releases (and I fear this could take weeks before we get it).
I agree we shouldn't hurry things. IMHO at least mathcomp should work. I am currently investigating what can be done (pinning things to commits and the like).
Right, I agree with you that there is no point to ping people if they don't have the tools to be able to test their package.
I will report status (in form of a package pick file) by tomorrow.
I guess it may be possible to test in CI with the lightweight Nix CI approach, but this still requires packaging 8.16+rc1 in Nix I believe
Progress is slow but steady. A quite common error is btw. something like:
The term "2" has type "GRing.Zmodule.sort ?t"
while it is expected to have type "nat".
Not sure if this has to be ...
@Michael Soegtrop I'm not sure I understand what you are doing? the current master branch of mathcomp compiles with 8.16+rc1, we should definitely do a release.
@Pierre Roux essentially I am testing for each package if it is sufficient to just patch allowed dependency versions (Coq and/or mathcomp) or if I need to pin the package to the latest commit on master. It is so far about half half for mathcomp. This is not a lot of work (I have automated scripts for that) but it takes time.
Of course a release of mathcomp would simplify things a lot, but then the policy should be to do a release when new / modified features are in good shape and not if a new Coq version came out. The reason d'être of Coq Platform is to give developers time to do proper releases.
So if you have no issues to do a release now, yes please go ahead. If there are issues which makes a release now not so nice, I can live with it.
BTW, if for some package the latest master commit does not work, a solution is to pick the commit from https://github.com/coq/coq/blob/v8.16/dev/ci/ci-basic-overlay.sh
Btw.: if I just need to relax dependency restrictions, I keep the package version number. If I have to patch it to a recent commit, the version is "preview". "preview" is different from "dev" in that it picks a specific tested to work commit (either latest master or as Théo mentioned from Coq's CI).
I agree the mathcomp release cycle is not ideal. I don't think there is any obstacle to releasing a 1.15, this will likely be done in the coming weeks (hopefully before the end of the month).
This would be perfectly fine for the Coq Platform release (planned early September), but end of the month would tighten the schedule for other developers, so I think it makes sense to continue my work and create a "patched to work" preview version for 8.16 which package maintainers can use to update their own packages.
I plan to release Coq Platform 2022.04.1 with 8.15.2 and 8.16.preview this week, latest on Monday.
I'm not sure I understand the need for a preview where maintainers have not been given the chance to do proper releases. For example, I wouldn't want aac-tactics for 8.16 to be based on some commit that just happened to work, even in a preview
I agree the mathcomp release cycle is not ideal.
I didn't say or mean that. In my opinion all Coq projects are independent and have the right to have their own release cycle, which is at least not very tightly tied to the Coq release cycle. For Coq Platform projects always have the option to either "patch up" the previous release, or to do a new release - whatever fits better.
Definitely I don't expect projects to do a release a week after the Coq release.
I do what I can to de-entangle the releases of Coq core and of Coq projects, so that maintainers can do quality releases rather than hurry releases.
@Karl Palmskog : the preview release is mostly there for package maintainers to prepare their releases - it is not intended for users. I personally don't like to use dev for that, because it breaks frequently. The preview release is more or less a frozen dev release.
Maybe we should find a better name for it.
Maybe we should call it dev-preview or dev-pick?
but how many maintainers are actually using a Coq Platform preview release to do testing? To me, the preferred venues of testing would be: manual opam based on the
core-dev opam archive, then Docker images, then Nix and other packaging tools
I expect that maintainers use opam and that they might find the local patch repo provided by Coq Platform useful, which provides a tested and stable set of package versions.
core-dev is not always fun to work with, first because it is not always stable and second because it might contain things which won't make it in the Coq Platform release.
But there are other reasons for doing this - I want e.g. to give the maintainers the information if their latest published release works with relaxed dependencies or not.
@Karl Palmskog @Pierre Roux : so what is the conclusion? Should I continue with this preview thing or should I ask people to use "dev" to develop their packages?
I'm not sure I understand what "using dev" entails exactly. We continually put actual releases of packages compatible with 8.16 into the
extra-dev opam repository as they arrive. If the package works with a stable Coq version as well, it can be put into the
released repository with version bounds that allow 8.16
then when 8.16.0 is released, we move every relevant release from
In my experience one can't build any larger set of packages this way, at most 2..3 packages. When they are more, always one package will require dev for Coq and/or mathcomp and that's it then.
Currently mathcomp is an example, it is either 8.15.2 + 1.14.0 or 8.16+rc1 + dev, which then pins most dependencies to dev as well.
What version of matchcomp do you suggest I should recommend package maintainers to use?
if their packages work with the last released MathComp and that MathComp works on 8.16+rc1, then they use that. Otherwise, they wait for a new release of MathComp
I personally think we should wait for a Docker image of 8.16+rc1. This is the main blocking point for releasing pretty much anything for 8.16 IMHO (I only released bignums because it is needed for the Docker image itself).
Tagging @Erik Martin-Dorel just so that he heards about that (no hurry)
Which as Pierre just said will take about 3 weeks - which is about half of the time we say we want to give package maintainers after a Coq release to adjust. And the dependency tree is in parts quite deep ...
@Pierre Roux : I think we need both, a docker image and a way to build packages with many dependencies (say VST) in a stable environment.
I lack experience on VST so I trust you here.
@Michael Soegtrop FYI, we now have 8.16+rc1 in Nix, which should help for the few mathcomp packages that use a Nix based CI.
Thanks - I am still struggling a bit with all the other packages, but can likely close this soon.
I wanted to ask if there is an update on the estimated arrival time for a 8.16 compatible release.
We have a meeting next wednesday (June 29th).
Last updated: Mar 02 2024 at 16:01 UTC