Stream: math-comp users

Topic: Coq Platform 8.16 preview release


view this post on Zulip Michael Soegtrop (Jun 07 2022 at 10:24):

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.

view this post on Zulip Théo Zimmermann (Jun 07 2022 at 10:30):

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.

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 10:33):

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).

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 10:34):

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 ...

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 11:30):

@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.

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 11:43):

@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.

view this post on Zulip Karl Palmskog (Jun 07 2022 at 11:49):

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.

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 11:53):

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).

view this post on Zulip Pierre Roux (Jun 07 2022 at 12:04):

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).

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 12:07):

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).

view this post on Zulip Théo Zimmermann (Jun 07 2022 at 12:08):

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.

view this post on Zulip Michael Soegtrop (Jun 07 2022 at 12:12):

I will report status (in form of a package pick file) by tomorrow.

view this post on Zulip Karl Palmskog (Jun 07 2022 at 12:45):

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

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 07:46):

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 ...

view this post on Zulip Pierre Roux (Jun 08 2022 at 08:04):

@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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:10):

@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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:10):

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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:10):

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.

view this post on Zulip Théo Zimmermann (Jun 08 2022 at 08:11):

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

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:12):

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).

view this post on Zulip Pierre Roux (Jun 08 2022 at 08:16):

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).

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:21):

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.

view this post on Zulip Karl Palmskog (Jun 08 2022 at 08:24):

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

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:25):

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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:26):

@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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:29):

Maybe we should call it dev-preview or dev-pick?

view this post on Zulip Karl Palmskog (Jun 08 2022 at 08:29):

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

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:35):

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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:41):

@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?

view this post on Zulip Karl Palmskog (Jun 08 2022 at 08:45):

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

view this post on Zulip Karl Palmskog (Jun 08 2022 at 08:46):

then when 8.16.0 is released, we move every relevant release from extra-dev to released

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:47):

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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:48):

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.

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:49):

What version of matchcomp do you suggest I should recommend package maintainers to use?

view this post on Zulip Karl Palmskog (Jun 08 2022 at 08:50):

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

view this post on Zulip Pierre Roux (Jun 08 2022 at 08:54):

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)

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:55):

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 ...

view this post on Zulip Michael Soegtrop (Jun 08 2022 at 08:58):

@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.

view this post on Zulip Pierre Roux (Jun 08 2022 at 11:02):

I lack experience on VST so I trust you here.

view this post on Zulip Pierre Roux (Jun 13 2022 at 13:04):

@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.

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

Thanks - I am still struggling a bit with all the other packages, but can likely close this soon.

view this post on Zulip Michael Soegtrop (Jun 25 2022 at 07:48):

I wanted to ask if there is an update on the estimated arrival time for a 8.16 compatible release.

view this post on Zulip Pierre Roux (Jun 25 2022 at 07:56):

We have a meeting next wednesday (June 29th).


Last updated: Feb 08 2023 at 07:02 UTC