update mathcomp packages #1243
update mathcomp packages #1243
Conversation
affeldt-aist
force-pushed
the
mathcomp-1.11.0+beta1
branch
from
cf36552 to
3ca9a4d
Compare
|
Wasn't there some kind of rule that said that beta versions were supposed to go into the |
|
This is a beta for users that we will keep as it is (so that users can build and rely on it), this is why we didn't put it in extra-dev (in our opinion extra-dev is for people who want to use the daily state of a repo). |
|
The issue is that, if a user naively types Before this pull request, only 3 packages had made the mistake of putting beta packages inside |
|
Is it okay to revert a commit in this repository? |
I would say yes, this has been done in the past (with |
|
This should be fixed by PR #1244. |
|
released versions should be in released. |
|
If it is not clear, please amend https://coq.inria.fr/opam-layout.html |
|
and just to be clear, extra-dev is for CI, you want beta packages to reach users. otherwise what is the point? I guess we should update the doc. |
No, it says: "The repository contains packages for development versions of external contributions to Coq. Typically .dev packages following the branches of the extension." Notice the word "typically". It is not written "only" or some other synonymous. It is written "typically"! And, as I already quoted, the "released" repository contains things that were "officially released". A beta version is not an official release. |
I'm very sorry the text is unclear. I wrote it. To me a beta is an official release, it is announced and has a version number. The point of splitting the repo is because .dev package change their contents depending on the upstream branch, read moon phase, so they are only useful for CI tracking a branch and not user consumption. I'm not a fan of repositories were all versions of a package stay (as OPAM does). At the beginning of the Coq+OPAM thing I proposed I much stricter layout, where we would have different repos for different Coq versions, only containing backward compatible updates. I did not manage to convince the others, so we got this hybrid model, where only .dev packages are segregated. Again, I'm not defending this model, but if you don't pick a specific version of a package it is always the case that We can discuss this better in the next Coq call, if you like @silene , but this was the model (poorly) described in the doc. I've never been the only one accepting PRs here, my bad I did not notice the misleading sentence before. |
Then explain to me why all the beta packages of Coq are in the
How come a beta version for Coq is a "development version", but a beta version for MathComp is an "official release"? The rules have to be the same for all the repositories! But maybe we should not be so focused on the repository for Coq. Let us see what happens in the outer world, e.g., the official Opam repository. For example, what about the beta versions for the OCaml compiler? They are in the official repository, but they depend on an For the sake of completeness, let me also mention the case of other packages: 1% of the packages actually put their beta versions in the official Opam repository (29 over 2630). And as far as I can tell, no beta versions have been added since the start of the year (but I may have missed one). |
|
To be clear, I'm fine amending the policy. |
for the release of version 1.11.0+beta1