[RFC] Repository layout for dev packages is problematic, turn `opam-coq-archive` into a single OPAM repository

ejgallego commented 1 year ago

Hi all,

as a follow up to the discussion on #2439 , I am opening this issue to propose and discuss a reorganization of opam-coq-archive, in particular to follow what is done with the OCaml compiler in the main Opam repository.

Motivation

The main motivation to write this proposal is that I've found the process for "beta" packages pretty cumbersome in the actual setup, both for users and maintainers.

By "beta" I mean versions that require Coq "rc" or "dev" versions.

Here's a couple of stories:

the extension author

F. has an application A that depends on the Coq's OCaml API, when a new Coq RC arrives, they are excited about letting users enjoy and test all the new features due to the RC new API. F. usually releases their package in the main opam repository, however the RC is only in core-dev.

Thus, F. prepares a package, and submits it to extra-dev; that is fine, however F. will have to react when the final Coq version is released to remove / move such package. This is a manual process, and F. will likely forget to update the package in extra-dev; moreover, the update is spurious, as F.'s package worked fine with the final Coq release. Moreover it makes F. to be aware of the coordination w.r.t. to the releases of a package they don't own.

Yet another problem F. faces is having to deal with two different package submission processes.

the adventurous user

G. is an adventurous user and they can't wait to try F's A, even if that means testing an RC version (which on the other hand seems interesting to them, as to ensure the new Coq will work fine in their setup)

G. has a setup with Coq + N packages from the released repository. In order to try "A"'s new version, G. must add new repositories core-dev and extra-dev.

That seems good to them, however they quickly realize that this update breaks havoc as their N packages want now to be updated to a strange version dev, moreover Coq itself wants to update itself to the dev version.

G. quickly learns that they must "pinning", however that process is very painful, and moreover, they don't have a good upgrade path for that switch when the final release happens.

Proposal

Indeed we can spot several problem in the above user experience: the need for manual pinning, duplication of packages among repositories, lack of stability / coordination with async release events required....

In order to remedy this I propose that the current set of repositories released / core-dev / etc... are unified into a single Coq repository; in this setup, "beta" packages are to be guarded by an "coq-beta" meta-package (as done in OCaml) that can be installed by several methods (including living in a special purpose repos)

Thus, foo.dev packages would live in the regular repos if needed.

Moreover, as an addon to the proposal, it could make sense to maintain the Coq beta packages directly in the main Opam repository.

Benefits

For the first part, the main benefit is that users would be able to try RC versions without needing any pinning or weird setup, other than installing the coq-beta package, and letting constraint resolution work. In general, I think this reduces the number of current manual steps and makes testing way easier.

Moveover, I'm unsure our usage of repositories as version markers is a use case really supported or encouraged by Opam, it has always felt weird to me, and I don't see any similar setup (in terms of deps) in other packaging systems.

Moving Coq beta packages to the main repository would have a few extra benefits:

dune-release would work for Coq out of the box
Coq RCs would benefit from OPAM CI setup
no more duplication of opam files across repos
packages willing to go to the main Opam repos can do so

Potential Problems

I've identified some preliminary concerns raised:

this could complicate the Coq platform setup, docker images: I fail to see how, it seems to me that it would make things simpler actually?
this could make testing beta versions of Coq too easy, generating load on maintainers: i think that making the testing of beta version easier is actually a very good thing, I'm a bit lost on the "generating load" part, as beta versions do pass CI so I'm unsure what kind of trouble the maintainers would suffer, but that's already the case today.

Some related issues:

gares commented 1 year ago

.dev packages were moved to dedicated repos because otherwise opam always wants to install these (as thy are the latest version) and this is not reasonable. Blocking them with a fake package is an option we did not consider back then.

Said that, I don't see how having just one coq-beta package would prevent opam from proposing random upgrades when one installs it to unlock the rc version of Coq

silene commented 1 year ago

The important piece of information is that the ocaml-beta package lives in a separate repository (and so would a coq-beta package). So, we still end up with two separate repositories: a normal one and a dev one.

palmskog commented 1 year ago

So, we still end up with two separate repositories: a normal one and a dev one.

According to our discussion in #2439, @ejgallego seemingly wants (contrarily to OCaml approach) to have everything to do with RCs live in the released repo, so that regular users can install RCs without doing anything but opam install coq-rcs or similar. I'm completely against this, not least for the reasons already outlined here by @gares.

silene commented 1 year ago

Then, the original post is quite misleading, because the very first sentence is: "to follow what is done with the OCaml compiler in the main Opam repository."

palmskog commented 1 year ago

If you look in other comments, there is the following one:

I'm unsure opam install coq-rc vs opam repos add make a lot of difference from the user or maintainer point of view

To me, the separate repo activation is absolutely crucial, and a main point in the OCaml approach to betas.

palmskog commented 1 year ago

To give some context on the extra-dev repo and RCs:

the only packages that currently have to live in extra-dev during the RC period are plugins - other packages will generally work with a released version of Coq, and can go in released even if they were targeting an RC
these extra-dev plugin packages for RCs are few in number, almost all part of the Coq Platform, and we track them in the opam archive repo and move them in batch to the released repo when the RC period is over
the RC period has not generally been all that long, up to a month or two, so it's probably better for general users to wait for the regular Coq release before trying one of the few plugins currently living in extra-dev

So I believe the proposal here tries to solve a problem that very few people have, with high risk of introducing Coq version opam upgrade chaos.

As to the Docker maintenance issues, the situation I really want to avoid is to have different sets of packages in Coq Docker images that are for RC versions of Coq and for released versions of Coq. For example, if only the RC image has the coq-rcs package and the regular Docker image does not, this is highly inconvenient. However, having different activated opam repos for RC and regular Docker images is something we already have, so that's fine.

ejgallego commented 1 year ago

Hi folks, actually OCaml is not using the beta-repository anymore, instead they use this:

flags avoid-version
depends
    "ocaml-beta" {opam-version < "2.1.0"}

I have also been told that the Coq platform is adding extra-dev but not core-dev so with some recent PRs that lead to a mess.

I'd suggest we discuss about this in the next Coq call.

ejgallego commented 1 year ago

So I believe the proposal here tries to solve a problem that very few people have, with high risk of introducing Coq version opam upgrade chaos.

That's a problem few people have now, but mainly because we are not doing a lot of development that requires people to test newer Coq versions.

ejgallego commented 1 year ago

According to our discussion in https://github.com/coq/opam-coq-archive/pull/2439, @ejgallego seemingly wants (contrarily to OCaml approach) to have everything to do with RCs live in the released repo, so that regular users can install RCs without doing anything but opam install coq-rcs or similar.

I'm sorry but this is not what I wrote there and neither in this issue, so you are confusing others.

What I wrote here is:

"beta" packages are to be guarded by an "coq-beta" meta-package (as done in OCaml) that can be installed by several methods (including living in a special purpose repos)

But funnily enough, OCaml is not doing this anymore as it doesn't work well, but I still would like to do what is done in OCaml which is to use avoid-version then.

I'm mostly concerned with packages that depend on the Coq API tho, as it is a similar problem that OCaml people had to resolve with their updated layout once they had to test stuff sensitive to compiler versions such as Merlin.

gares commented 1 year ago

So which is your conclusion @ejgallego ? what are you proposing on the end? A single repo with avoid-version or what?

silene commented 1 year ago

Note that avoid-version is only available since Opam 2.1, which is quite recent. That is why even the most recent Opam packages (e.g., rc of OCaml 5) still use depends: ocaml-beta (possibly with { opam-version < 2.1.0 }) and they will continue to do for several years to avoid spuriously installing beta packages on systems still managed by Opam 2.0 (as it ignores the avoid-version flag).

gares commented 1 year ago

OK, it seems sensible to follow what ocaml does then (I mean use a separate repo for the beta package until all opam versions in use support the new flag)

ejgallego commented 1 year ago

Sorry folks, I've moved the topic to Coq's Call next week, I can't make it today. I will answer to Enrico's question ASAP.

ejgallego commented 1 year ago

So which is your conclusion @ejgallego ? what are you proposing on the end? A single repo with avoid-version or what?

Thanks @gares for asking the question as indeed while I am aware of the problems we have now, the solution was not clear, but I've given it a bit of thought now.

Please find below and updated proposal based on the discussions we've had here; let me remark that this is just a proposal and I think we have quite a few degrees of freedom on tweaking it, so hopefully we can discuss in the call and refine it more until we reach something that makes everyone happy (and the current problems go away)

So what I think makes most sense now is:

remove the core-dev repository. All coq packages live in the main opam repos, and experimental packages have the avoid-version , coq-beta package as done in OCaml upstream.
move all the non-dev packages in extra-dev to released, these are mainly the packages done for rcs and the ones that motivated this issue, such packages are also tagged avoid-version
keep the dev repos, until Opam provides a fully working opam pin add $pkg --dev, but add avoid-version to all of them
fix the platform depending on extra-dev
improve coq as to be a virtual package, so we can provide variants (this is useful for those of us that require extra backports of master features

It seems to me that this model has good properties:

no more moving of packages among repos: now all packages have a canonical location, and no package is duplicated
packages that work for an rc version don't need an update for the final release (unless there is an API change between the RC and the final coq version)
no pin is needed anymore for most combinations, including the dev repository

WDYT?

coq / opam