[coq-lsp] 0.1.3 release for 8.17

[ejgallego]

No description provided.

[palmskog]

I will assume that you move this and 0.1.2 to the regular opam repo (and thus delete from here) once 8.17.0 is out.

[ejgallego]

I will assume that you move this and 0.1.2 to the regular opam repo (and thus delete from here) once 8.17.0 is out.

Sure, if that's the right thing to do, tho indeed the workflow for packages that would like to work against RC seems a bit complex then, as they need to move to released after the RC is done, but the packages themselves have not changed.

Maybe RC versions should instead go to released directly, as OCaml does, and have it depend on a coq-beta package, but I'm not sure how much special case for OCaml opam already has.

[palmskog]

We have the general assumption that the released repo should be completely self-contained, i.e., not require any other repo besides the general OCaml one (opam-repository). So if we want to have things depending on an RC in released then we need to put RC versions of Coq into opam-repository. This leads to more work for volunteers, and people will get the not-so-well-tested RC if they do opam install coq.

Here, I meant that these packages should probably migrate to opam-repository rather than released, since that's where you put the 8.16 release for coq-lsp.

[ejgallego]

What I mean is putting the Coq RCs themselves into released, as OCaml does.

The trick they use is that RC versions depend on ocaml-beta so users are not upgraded to RCs unless they have opted in.

Does it make sense?

[palmskog]

Putting RCs directly into released doesn't make any sense to me, since we then expose every Coq user to it (opam install coq) and make them upgrade to it if they do opam upgrade coq.

It could make sense if we introduce some new virtual package like coq-candidate or similar (RCs are not betas). But it will complicate everything from the Platform to the Docker images, so it needs careful discussion akin to that for coq-native.

[ejgallego]

Putting RCs directly into released doesn't make any sense to me, since we then expose every Coq user to it (opam install coq) and make them upgrade to it if they do opam upgrade coq.

As I've mentioned for that to happen you'd need to have the coq-beta package installed, as OCaml does.

But it will complicate everything from the Platform to the Docker images, so it needs careful discussion akin to that for coq-native.

What complication would have?

The current setup seems more complex to me, as if I want to use / test and RC I need to:

1. add a repository, with lots of random dev packages I don't care about
2. pin the package(s) , as dev is higher than any RC

Moreover a lot of packages that may be in release and work fine with the new version are now in a cross-dep setup with the stuff in dev, so I dunno.

[palmskog]

As I've mentioned for that to happen you'd need to have the coq-beta package installed, as OCaml does.

Yes, I was saying that without some virtual package, it doesn't make any sense to me.

One obvious complication is that some Docker images will suddenly need to have a virtual package coq-candidates installed, while some don't, and we need to juggle Docker tags like 8.17 from depending on the virtual package to not depending on it as Coq versions get released.

And everyone will need to think about whether they want to be in conflict with coq-candidates (I certainly would want my packages to be in conflict, I don't want complaints from users with non-released versions of Coq).

[palmskog]

If you want to follow OCaml, why not put all RCs in a new separate repo? https://github.com/ocaml/ocaml-beta-repository

This is an opam repository that contains beta releases of the OCaml compiler. It is in a separate opam remote from the stable opam-repository so that the beta compilers are an opt-in for advanced users.

This is to me a much better solution than intermingling regular and RC-related packages.

[ejgallego]

This is to me a much better solution than intermingling regular and RC-related packages.

OCaml abandoned this approach long time ago, in favor of the one I'm describing now, because indeed there are a few problems with that approach, in particular stability and cross-repos dependencies, among others.

Yes, I was saying that without some virtual package, it doesn't make any sense to me.

Yes, this whole setup needs options.

One obvious complication is that some Docker images will suddenly need to have a virtual package coq-candidates installed, while some don't, and we need to juggle Docker tags like 8.17 from depending on the virtual package to not depending on it as Coq versions get released.

How is that different from today? Today the docker images for beta need to take some extra step, in fact it would be simpler if the docker image could just say PKGS=coq-rc no?

And everyone will need to think about whether they want to be in conflict with coq-candidates (I certainly would want my packages to be in conflict,

Nobody should be in conflict with coq-rc , why would be? Packages should just declare their correct version bounds.

I don't want complaints from users with non-released versions of Coq

That's fine, but IMHO the package manager is not the place to enforce it.

[palmskog]

OCaml abandoned this approach long time ago, in favor of the one I'm describing now, because indeed there are a few problems with that approach, in particular stability and cross-repos dependencies, among others.

If you look at https://ocaml.org/news/ocaml-5.0.beta2 they have the following line:

opam switch create 5.0.0~beta2 --repositories=default,beta=git+https://github.com/ocaml/ocaml-beta-repository.git

So clearly that repository is being used still.

How is that [virtual package] different from today?

Right now, everything is handled with regular Coq pinning and selecting which opam repositories to include. There are no dev-specific packages.

[ejgallego]

So clearly that repository is being used still.

Indeed the meta-package ocaml-beta lives there, I guess they wanted some extra safety net as not to allow people install ocaml-beta accidentally? But other than that, all the packages live in the main repos.

Still, adding the ocaml-beta repos won't cause the problems adding the core-dev repos for Coq, in particular, it won't try to upgrade anything unless I also install the package.

The problem with pinning is that it may not scale, but the setup is indeed subtle. Let's compare testing a RC with the coq-lsp use case.

Case 1, using the current setup:

• Add core-dev and extra-dev
• Now we need to pin both coq and coq-lsp to the right versions, with the problems that it entails.
• Moreover I may need to pin all the regular packages I'm using, and here is the key point, many of these packages like coq-mathcomp-ssreflect have depends: [ "coq" {>= "8.13"} ] so they need to be pinned

So the problem with that is mainly scalability of pinning, and in general the setup seems brittle to me.

Case 2, using an OCaml-like setup:

• Install the coq-rc metapackage, it may live in a separate repos for safety
• everything works out of the box with opam update no pinning necessary

[palmskog]

Yes, I'm aware of how it works with core-dev and extra-dev. I'd be prepared to live with the OCaml meta-package-in-other-git-repo approach, since it ensures that regular users are completely unable to install any RCs. But I'm absolutely against any approach where regular users of released can just install a meta-package and get RCs without adding a git opam repo. Then, I guarantee I'd add a meta-package conflict for all packages I manage.

[ejgallego]

Yes, I'm aware of how it works with core-dev and extra-dev. I'd be prepared to live with the OCaml meta-package-in-other-git-repo approach, since it ensures that regular users are completely unable to install any RCs.

It seems to me that we are mixing two things here:

• how well the current setup works, and whether we are happy with it for example for coq-lsp, this is a opam-repos specific issue
• how to express preferences of maintainers wrt their set of supported configurations

That last one, has I think little to do with opam-repos and people can (and do) install packages from many different sources / ways.

Going back on the first topic, what do you think of the current setup, do you think it is workable?

But I'm absolutely against any approach where regular users of released can just install a meta-package and get RCs without adding a git opam repo. Then, I guarantee I'd add a meta-package conflict for all packages I manage.

I'm unsure opam install coq-rc vs opam repos add make a lot of difference from the user or maintainer point of view, I'm also not sure what is your support policy.

When do you exactly support your packages with pre-release versions?

[palmskog]

There are many more concerns here than you're mentioning, such as the support burden of Coq RCs that live on forever and are easy to install (get pulled in) by accident.

My main concern is always the combination of opam-repository + released. I think the Platform shows that the combination works well, and this is a strong argument for keeping released self-contained / independent of any other repo than opam-repository.

core-dev and extra-dev work well for the purposes I personally use them for, which is testing stuff on a zoo of Coq versions with a lot of pinning. I tag some of my packages during RCs, put them in extra-dev for testing, and then move them to released when RC period is over. Works fine for me.

Even if you feel RC pinning is an issue as per above, still the only proposed solution I'd be fine with is the OCaml meta-package-in-other-git-repo one. I think the difference between opam install and opam repo add is really significant.

[ejgallego]

There are many more concerns here than you're mentioning, such as the support burden of Coq RCs that live on forever and are easy to install (get pulled in) by accident.

How would that accident happen? Do you have an example?

How are these a support burden as compared to the current situation?

[Note that I don't care if we require opam install coq-rc or opam repos add coq-beta, I only see a very small difference here]

My main concern is always the combination of opam-repository + released.
I think the Platform shows that the combination works well, and this is a strong argument for keeping released self-contained / independent of any other repo than opam-repository.

Yes, current released works reasonably well here, what seems to work pretty painfully is using the RC versions and making an RC platform.

core-dev and extra-dev work well for the purposes I personally use them for, which is testing stuff on a zoo of Coq versions with a lot of pinning. I tag some of my packages during RCs, put them in extra-dev for testing, and then move them to released when RC period is over. Works fine for me.

Works fine for you [the overhead seems already large to me tho, but that's a different issue]

But I'm worried about a different use case, when a user for example wants to try a RC version and the corresponding coq-lsp for that version. The current setup seems really bad to me, both as a user and as maintainer.

Moreover, it relies on a lot of manual stuff that won't just scale if the archive grows larger. Why should I have to move the coq-lsp packages to the released repos. They should work fine when 8.17 is released too.

Even if you feel RC pinning is an issue as per above, still the only proposed solution I'd be fine with is the OCaml meta-package-in-other-git-repo one. I think the difference between opam install and opam repo add is really significant.

Unless you tell me a bit more about what the support policy of your packages, I can't follow you here.

What I've gotten so far is "if user install a RC with command A, then I'm fine, but if they install the RC with command B, then I need to add conflict with all RC versions".

Is that what you mean?

[palmskog]

But I'm worried about a different use case, when a user for example wants to try a RC version and the corresponding coq-lsp for that version. The current setup seems really bad to me, both as a user and as maintainer.

RCs are meant for testing Coq and testing of Coq packages against the RC. It's not for regular users who just want to try some package.

Unless you tell me a bit more about what the support policy of your packages, I can't follow you here.

I don't want to deal with any support requests for released packages on any non-released version of Coq. Non-released versions of Coq include RCs. If it is made possible via released for regular users to use RCs without a barrier like a separate opam repo, then I will have to prevent installation on RCs via conflict clauses.

[ejgallego]

RCs are meant for testing Coq and testing of Coq packages against the RC. It's not for regular users who just want to try some package.

I was not aware of this idea about RCs, when we proposed the current RC system for Coq for sure we had in mind to have these versions tested widely. Nowadays the CI makes that role for non-interactive testing.

However, there are quite a few packages such as IDEs or indexers, (or even linters) that can benefit from testing. For coq-lsp, I often get feature requests, and I need an easy way for the users to try their normal setup with a "dev" version of Coq + coq-lsp for example.

I don't want to deal with any support requests for released packages on any non-released version of Coq.

Sure, that makes sense.

Non-released versions of Coq include RCs. If it is made possible via released for regular users to use RCs without a barrier like a separate opam repo, then I will have to prevent installation on RCs via conflict clauses.

It is now possible for users to do that very easily today, so I fail to see how my proposal makes things different, for the users, they are just running a command.

Preventing installation of packages together with a Coq RC seems like a really bad thing to me, how are devs and users supposed to test new stuff? Not to say of the overhead you are adding to the maintenance process. Imagine having this kind of restriction for something like OCaml 5...

I think your bug reporting system should instead be where the guard is, filter out versions that you don't want to support.

[palmskog]

It is now possible for users to do that very easily today, so I fail to see how my proposal makes things different, for the users, they are just running a command.

Then it should super easy for you to convince the OCaml people to drop https://github.com/ocaml/ocaml-beta-repository and allow betas everywhere. Let's make this a necessary but not sufficient condition for our adoption of something similar.

[ejgallego]

Then it should super easy for you to convince the OCaml people to drop https://github.com/ocaml/ocaml-beta-repository and allow betas everywhere. Let's make this a necessary but not sufficient condition for our adoption of something similar.

Sorry if I wasn't clear, I'm very happy with having the extra repos with the enabling package as done in OCaml and in the way you prefer.

I was just curious about why you folks considered it an important safeguard; for me, one solution or the other don't make a big difference, so I'm very happy with having coq-beta or whatever that could be named in its own repos.

[ejgallego]

Actually OCaml upstream is not using the ocaml-beta stuff anymore, but the avoid-version flag new in Opam 2.1, interesting.

[palmskog]

We have hundreds of users reporting problems running various parts of the Coq ecosystem across many forums, and the support process usually begins with figuring out how they install Coq and packages. Having only a few ways to install released Coq properly is a crucial way we can limit the support burden.

My message from the opam archive has consistently been that the released repo is well supported together with Coq from opam-repository, but anything else like core-dev is for devs and experimenters only, and even basic questions are likely to be unanswered.