Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

remove coq-iris.dev and coq-stdpp.dev #2256

Merged
merged 1 commit into from
Aug 17, 2022
Merged

Conversation

RalfJung
Copy link
Contributor

@RalfJung RalfJung commented Aug 17, 2022

These packages were added without our consent in #2080. They cause problems because we have a | "dev" dependency in all our packages to easily be able to pin a locally patched version of the package. If such a dev package exists in any repository, opam will install it automatically sometimes (in particular when it cannot find other ways to resolve the version constraints), which is never intended -- these packages should only ever be installed by hand. This actually happened last week where our CI succeeded when it should have failed due to a version conflict.

Cc @MSoegtropIMC -- I don't know why you added those packages, but I hope we can find a way to resolve your use-case with fewer side-effects.

Also I would ask the opam-coq-archive maintainers to not merge coq-stdpp/coq-iris packages that do not come from the std++/Iris team (unless they are just obvious bugfixes). This is the 2nd time that happened.

@palmskog
Copy link
Collaborator

palmskog commented Aug 17, 2022

@RalfJung we only perform lightweight reviewing of extra-dev packages, and it's easy for packages to slip by. Can you please define clearly how to check if something "come[s] from the std++/Iris team"? We have no way of knowing who all the members are, and if/whether they use some predictable metadata in their packages.

@RalfJung
Copy link
Contributor Author

RalfJung commented Aug 17, 2022

we only perform lightweight reviewing of extra-dev packages, and it's easy for packages to slip by

Yeah, I understand. I appreciate the work you are putting in to maintain these repositories. :)

Can you please define clearly how to check if something "come[s] from the std++/Iris team"?

Fair question. For now we can just say that @robbertkrebbers or me should approve such PRs.

@MSoegtropIMC
Copy link
Contributor

@RalfJung : this is a requirement of Coq Platform CI. I regularly run dev builds of Coq Platform to check if the master (or whatever dev points to) version of packages Coq Platform uses works, so that I can see issues early at the horizon. It would not be much effort to remove iris from Coq Platform dev CI testing, but I wouldn't like to do this, since iris is a rather large and fundamental package.

As Karl said, the extra-dev repo is generally considered to be there for Ci / test / expert user purposes and usual acknowledge hurdles don't apply here (as they do to released).

I hope we can find a solution which suites both our needs.

@anton-trunov
Copy link
Member

FWIW, GitHub supports this feature called CODEOWNERS (see https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners): it lets one specify who owns which directory/file in this repository and default code owners too. The code owners will be automatically notified to review PRs touching the parts of the code base they own. Perhaps this could be useful for cases like this one.

@palmskog
Copy link
Collaborator

palmskog commented Aug 17, 2022

@MSoegtropIMC since these packages are causing issues, could we maybe move the Stdpp/Iris dev packages to the Platform's overlay for opam-coq-archive? That is, could we merge this PR and then discuss a workaround in some other place?

A solution based on CODEOWNERS could work, but here we sort of want to say that certain directories that don't exist shouldn't exist. So it's a bit more complicated.

@palmskog
Copy link
Collaborator

@RalfJung OK, I will go with the following rule of thumb: whenever I see a package that looks directly related to Iris / Stdpp, I will ping you and Robbert in to comment (but there will be a timeout, maybe a couple of days, after which I will use my own judgment if I don't hear back).

@MSoegtropIMC
Copy link
Contributor

@palmskog : the not so nice side of local dev packages is that I don't get updates when dev packages are pinned, but then this doesn't happen that frequently currently. So if there is no other solution, having a local dev package is fine with me.

@RalfJung
Copy link
Contributor Author

RalfJung commented Aug 17, 2022

@MSoegtropIMC the way I would recommend that people install the latest dev version of std++ and Iris is via

opam pin add coq-stdpp.dev git+https://gitlab.mpi-sws.org/iris/stdpp/
opam pin add coq-iris.dev git+https://gitlab.mpi-sws.org/iris/iris/
opam pin add coq-iris-heap-lang.dev git+https://gitlab.mpi-sws.org/iris/iris/

Does that work for your CI? It has the big benefit of avoiding side-effects via global shared state such as this repository. It also means you automatically get updates when we change our opam files (whereas the .dev packages in this repo would bitrot, since we are not maintaining them).

Another option would be to set up a small repo with the dev packages you need; that's what we do for Iris development (https://gitlab.mpi-sws.org/iris/opam/). That runs the risk of the opam files becoming outdated, but they rarely change.

the not so nice side of local dev packages is that I don't get updates when dev packages are pinned

You wouldn't get updates for the .dev packages in extra-dev either.

@palmskog

OK, I will go with the following rule of thumb: whenever I see a package that looks directly related to Iris / Stdpp, I will ping you and Robbert in to comment (but there will be a timeout, maybe a couple of days, after which I will use my own judgment if I don't hear back).

That sounds like a reasonable policy. Even if we only get around to look at this after your timeout, at least we'll have the notification in our queue, so we know something happened. This time, I spent 10min or so debugging until I even considered the option that there might be new std++ packages in the opam repo that I did not add.

@palmskog
Copy link
Collaborator

OK, then I think we merge this PR and continue to think about solutions to the general problem in other issues and on Zulip.

@palmskog palmskog merged commit 07667b4 into coq:master Aug 17, 2022
@RalfJung RalfJung deleted the no-iris-dev branch August 17, 2022 12:48
@MSoegtropIMC
Copy link
Contributor

Btw.: IMHO the correct solution to this would be to have a dev package naming such that in version comparisons dev < released, so that opam won't pick a dev package unless explicitly requested if a release package would work. I find it rather inconvenient that dev is considered > releases.

@RalfJung : it would be a bit of work to handle this, but doable, and likely a good solution.

@MSoegtropIMC
Copy link
Contributor

@palmskog : yes please go ahead.

@ybertot
Copy link
Contributor

ybertot commented Aug 17, 2022

Following on @anton-trunov's idea, it would be enough to ascribe the right code owners to directories opam-coq-archive/extra-dev/packages/coq-iris and opam-coq-archive/released/packages/coq-iris. Could this work?

I understand that opam-coq-archive/extra-dev/packages/coq-iris/coq-iris.dev should not exist, but we could have a opam-coq-archive/extra-dev/packages/coq-iris/coq-iris.dummy to justify the existence of opam-coq-archive/extra-dev/packages/coq-iris

@MSoegtropIMC
Copy link
Contributor

My expectations are that the restrictions even work when the directory does not exist.

@RalfJung
Copy link
Contributor Author

Btw.: IMHO the correct solution to this would be to have a dev package naming such that in version comparisons dev < released, so that opam won't pick a dev package unless explicitly requested if a release package would work. I find it rather inconvenient that dev is considered > releases.

That wouldn't help. We usually have dependencies of the form

  "coq-stdpp" { (= "dev.2022-08-16.0.0ccf17a1") | (= "dev") }

so the order already doesn't matter, it's all equality constraints.

We find that the only way to ensure that reverse dependencies keep building is by always using a particular version -- there are just way too many changes that can cause a reverse dependency to break, so inequality constraints are too fragile.

it would be a bit of work to handle this, but doable, and likely a good solution.

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants