Karl Palmskog (Dec 18 2020 at 18:14): Karl Palmskog (Dec 18 2020 at 18:14):it seems we will see this list grow with 8.13 packages in extra-dev: https://github.com/coq/opam-coq-archive/projects/1
For the 8.13 platform, I recommend copying these packages into the 8.13 branch at earliest opportunity
Michael Soegtrop (Dec 18 2020 at 20:21):I don't understand in detail what you mean.
Karl Palmskog (Dec 18 2020 at 20:35):for example, the aac-tactics opam package in the 8.13 platform branch is nonsense. The proper one is this, so please use it: https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-aac-tactics/coq-aac-tactics.8.13.0/opam
Michael Soegtrop (Dec 18 2020 at 20:40):@Karl Palmskog : then we should delete them from the coq platform v8.13 branch and add the extra-dev repo. Currently the v8.13 branch has these repos:
<><> Repository configuration for switch _coq-platform_.8.13.0+beta1 ><><><><><>
1 patch_coq-platform_.8.13.0+beta1 file://T:/bin/test_8_13_beta_32_a/home/Michael/coq-platform/opam
2 coq-released https://coq.inria.fr/opam/released
3 coq-core-dev https://coq.inria.fr/opam/core-dev
4 default git+https://github.com/fdopen/opam-repository-mingw.git#opam2
Not sure what would be the best order. @Enrico Tassi : can you explain your rationale for the repo order?
The platform opam repo should always only be temporary.
Karl Palmskog (Dec 18 2020 at 20:45):our CI only for the released repo targets only released versions of Coq, so it doesn't make sense to have packages that only support 8.13 there. Therefore, we "park" them in extra-dev, and move them to released unchanged when 8.13.0 is out.
Michael Soegtrop (Dec 18 2020 at 20:49):So wouldn't it make sense to add the extra-dev repo to the repo list of Coq platform 8.13.beta? Then if 8.13.0 is released, the packages are moved to the released repo and we remove the extra-dev repo from Coq platform.
Karl Palmskog (Dec 18 2020 at 20:52):for 8.13.beta, it could make sense to add extra-dev, sure. As long as you remove it in the 8.13 platform release
Karl Palmskog (Dec 18 2020 at 20:53):I'm not sure the repo order will matter. The repos are supposed to be disjoint (released INTERSECTION extra-dev is empty, in terms of exact packages+versions, but there are additional versions in extra-dev of some packages in released)
Michael Soegtrop (Dec 18 2020 at 21:06):Yes, that's the idea. Have core-dev and extra-dev in the beta of the platform and remove it in the release. The only issue is that platform wouldn't build while the packages are moved from extra-dev to released.
Karl Palmskog (Dec 19 2020 at 10:42):I can flag up when we do the move to released so you can deactivate extra-dev at the same time.
Michael Soegtrop (Dec 19 2020 at 11:18):Yes, this would be helpful. Anyway, an outage of the platform beta shortly after the release shouldn't be an issue.
Théo Zimmermann (Dec 19 2020 at 11:43):If you also include the released repo in the platform beta, why would it ever stop working?
Enrico Tassi (Dec 19 2020 at 12:45):IMO for 8.14 we should try the converse:
releasedreleased (e.g. coq-elpi 1.8.1)released and its own overlay, so that the final user is not exposed "developmet versions" by default (once the platform is installed and the does opam install X)released is supposed to be self contained) Enrico Tassi (Dec 19 2020 at 12:49):My opinion is that *-dev repositories are there for CI/perf/automation only, it's not something the user should see.
At the same time coq.xX.beta is a released version (has a version number) so should be in released, but we don't want users to be installing the beta without wanting that. Here the trick suggested by Guillaume can help us. If we put coq.xX.beta in released but we make it depend on a fake package coq-beta-testing which is in core-dev only people who explicitly opt in will get it (by using the core-dev repo or telling opam to ignore the dependency).
Enrico Tassi (Dec 19 2020 at 12:51):In some sense today we put the beta versions of Coq in core-dev for the wrong reason, and this forces other packages to be uploaded there and then moved back to released.
Karl Palmskog (Dec 19 2020 at 12:57):so now we're going to have a bunch of betas in released? I'm against this, whether you use the virtual package stuff or not
Enrico Tassi (Dec 19 2020 at 12:57):For 8.13 I think I can do the move to released and then fix/update the platform on the same day of the release, I hope I will manage.
Enrico Tassi (Dec 19 2020 at 12:58):Elpi 1.8.1 is not a beta, but is in extra-dev, is it OK in you opinion?
Karl Palmskog (Dec 19 2020 at 12:58):it's in extra-dev for the simple reason that it doesn't build with any released Coq version
Michael Soegtrop (Dec 19 2020 at 13:02):If you also include the released repo in the platform beta, why would it ever stop working?
Indeed, that's right. I will add the extra-dev repo and see what packages can be removed / should be moved to extra dev.
Enrico Tassi (Dec 19 2020 at 13:05):Well, I guess we have to agree on what "released" means. The doc I wrote a long ago is not ruling out betas
The repository contains packages for Coq and for Coq extensions that were officially released by the Coq team or their corresponding authors. All packages have a version number (i.e. no .dev packages). The repository is self contained. The repository is intended to be used by people familiar with the OPAM tool.
To me a beta is an official release, we announce it, we make packages... and has a version/tag
have a bunch of betas in released? I'm against this
It may help to explain what problem you see. The problem I see with the current approach is that we have to put things in the wrong place and then move them in the right place. It is not the end of the world, but does not seem right either.
Karl Palmskog (Dec 19 2020 at 13:06):on GitHub, betas are marked as pre-releases, not real releases
Enrico Tassi (Dec 19 2020 at 13:07):And what is the problem with having in released also "pre-releases"?
Karl Palmskog (Dec 19 2020 at 13:07):I think we already have enough problems correcting issues with packages in released that target actual Coq releases. Betas don't have a good track record when it comes to bugs, incompatibilities, etc.
Paolo Giarrusso (Dec 19 2020 at 13:12):Also, a library compatible with Coq >= 8.11 shouldn’t be expected to be compatible with betas in that range, no?
Karl Palmskog (Dec 19 2020 at 13:12):I think this is similar to coq-native by default. Personally, if betas/rcs became "real" releases, I would add opam requirement conditions so my projects can't be built with them, and advise others to do the same.
Karl Palmskog (Dec 19 2020 at 13:14):Paolo Giarrusso said:
Also, a library compatible with Coq >= 8.11 shouldn’t be expected to be compatible with betas in that range, no?
with Enrico's solution, libraries that say they are compatible with 8.14 (e.g., >= "8.14") would implicitly say they are compatible with betas as well, unless they took special care to not be.
Enrico Tassi (Dec 19 2020 at 13:14):If it is not compatible with the beta, why then would it be compatible with the final? I see your point, but it has more to do with being open-ended in the constraints than the beta thing no?
Karl Palmskog (Dec 19 2020 at 13:16):from a Coq project maintainer's perspective, there seems to be no significant upside to allow compatibility with a beta/rc, and plenty of downside in that users may complain if it doesn't build
Enrico Tassi (Dec 19 2020 at 13:17):if the beta is not installed by default, then I don't see the build problems coming
Paolo Giarrusso (Dec 19 2020 at 13:20):Betas aren’t reliably compatible with final releases. Even dot releases aren’t in practice. That’s why a project could be compatible with a final release and not a beta.
Karl Palmskog (Dec 19 2020 at 13:23):@Enrico Tassi are you talking now as a Coq dev team member with having betas in opam (whether the official one or released)? Because the current status is that opam packaging even of Coq itself is considered outside the duties of a release manager and handled by volunteers. If the new beta regime with opam is something that the Coq dev team and release managers want, it seems fair that they take over all Coq opam packaging first.
Enrico Tassi (Dec 19 2020 at 13:29):I think you are warming up too much @Karl Palmskog , you made you position clear: you don't like my proposal. Fine.
Karl Palmskog (Dec 19 2020 at 13:30):I think one issue is that Coq opam volunteers and dev team interests are somewhat diverging
Paolo Giarrusso (Dec 19 2020 at 13:31):@Enrico Tassi can the problem be solved some other way?
Karl Palmskog (Dec 19 2020 at 13:31):one of the main motivations for me with helping out with released is getting packages certified with real Coq releases
Enrico Tassi (Dec 19 2020 at 13:31):Betas aren’t reliably compatible with final releases.
Well, my hope it to make this wrong in the future. In 8.12 the diff between V8.12+beta1..V8.12.0 is minimal, in 8.13 it's empty so far. If it continues like that, I guess you can see why my proposal is not absurd. But I understand we need more time to make this the default and not the exception.
Enrico Tassi (Dec 19 2020 at 13:32):Yes, we can just move 5 packages from one directory to another one on the release day.
Enrico Tassi (Dec 19 2020 at 13:32):It's not a big deal, so far.
Paolo Giarrusso (Dec 19 2020 at 13:33):that the 8.12 diff was so small is a bug, not a feature.
Enrico Tassi (Dec 19 2020 at 13:33):What do you mean?
Paolo Giarrusso (Dec 19 2020 at 13:33):because of all the bugs fixed in 8.12.1 and 8.12.2.
Paolo Giarrusso (Dec 19 2020 at 13:34):I think your goal is to discover and fix those bugs earlier — by 8.12.0.
Paolo Giarrusso (Dec 19 2020 at 13:34):because the beta would get more testing.
Enrico Tassi (Dec 19 2020 at 13:34):If we stick to a "time based released" then I don't see how you can expect bugs to be reported and fixed when you like, and not when they happen to be ;-)
Enrico Tassi (Dec 19 2020 at 13:35):Indeed, I'd love to, but it did not happen. Now I asked myself why
Paolo Giarrusso (Dec 19 2020 at 13:35):I think that’s exactly what’s good about your proposal.
Paolo Giarrusso (Dec 19 2020 at 13:35):if 8.12 had followed your process, beta1 would have been the same but could have gotten more testing.
Enrico Tassi (Dec 19 2020 at 13:36):Maybe, but this is not what I'd like to do.
Paolo Giarrusso (Dec 19 2020 at 13:36):then, _some_ of those bugs would have been _discovered_ earlier.
Paolo Giarrusso (Dec 19 2020 at 13:36):oh?
Karl Palmskog (Dec 19 2020 at 13:36):I'm open to discussion how we can get more testing of betas or rcs by people in general, but so far 8.12 seems unique in that it didn't have major problems in the beta, which is why I think having betas in core-dev still makes sense
Enrico Tassi (Dec 19 2020 at 13:36):This thread is about uploading a few packages in one archive rather the other one.
Paolo Giarrusso (Dec 19 2020 at 13:37):sorry, I assumed this was also related to the beta changes.
Karl Palmskog (Dec 19 2020 at 13:38):I think it is related, in some wider sense.
Enrico Tassi (Dec 19 2020 at 13:39):I promised to write down a summary of how I see the release process should change, but I had no time so far.
In short, I'd like hotfixes (point released) to come out very fast and be super conservative about them (fixes which are really needed, not arbitrary changes). The point being that between the beta and the final we have very little feedback (for many reasons).
Enrico Tassi (Dec 19 2020 at 13:39):So the classical "beta period" thing is not helping much, not working as one expects.
Enrico Tassi (Dec 19 2020 at 13:40):For once it is very short, and you may not have all you need to test your project...
Karl Palmskog (Dec 19 2020 at 13:41):from the other side of the fence, as we have gotten much better CI facilities, testing lots of projects with an alpha and beta has become easier. The main issue for me whether I test an alpha or beta is usually CI availability
Enrico Tassi (Dec 19 2020 at 13:41):So we need better CI so that we can, from the start, tag something worth being called final.
Enrico Tassi (Dec 19 2020 at 13:41):totally agree
Karl Palmskog (Dec 19 2020 at 13:42):but to me at least, the CI stuff is independent of whether it [the alpha or beta] lives in released or core-dev, since Erik handles that in his Docker images
Paolo Giarrusso (Dec 19 2020 at 13:43):And FWIW: I thought one of the (laudable) goals was also to enable more testing for betas. But that would reveal more of the existing bugs, and make beta and final releases diverge wider, invalidating some of the assumptions.
Enrico Tassi (Dec 19 2020 at 13:43):My proposals turns the "beta period" into "platform beta period", so that when Coq tags the final we have a real platform (in beta). So that people can test things. And if there is a bug in Coq, we make an hot fix and rebuild the platform (in 2 days max).
Paolo Giarrusso (Dec 19 2020 at 13:46):Sounds great, and should have the effects I was expecting, including some earlier bug reports and more divergence. Maybe even earlier fixes, but that’s dev-time-limited.
Paolo Giarrusso (Dec 19 2020 at 13:47):But maybe beta and final would stay compatible, if the “platform beta” increases test coverage.
Paolo Giarrusso (Dec 19 2020 at 13:48):bugs specific to interactive use might not get caught by the beta, but those fixes seem indeed more likely to be backward compatible.
Enrico Tassi (Dec 19 2020 at 13:49):I mean, there is no much difference, from a VCS standpoint, between Xbeta1, Xbeta2, Xfinal, Xpoint1, ... and X, Xpoint1, Xpoint2... But if Xfinal the thing that makes the thing testable, then I think it may be worth doing the right-shift (as much as possible).
The organization of the opam archive is mostly orthogonal to this, at least to my eyes.
Enrico Tassi (Dec 19 2020 at 13:51):Paolo Giarrusso said:
bugs specific to interactive use might not get caught by the beta, but those fixes seem indeed more likely to be backward compatible.
even more when we switch to a standard protocol...
Paolo Giarrusso (Dec 19 2020 at 13:51):I guess the only link is > If it is not compatible with the beta, why then would it be compatible with the final?
Paolo Giarrusso (Dec 19 2020 at 13:52):So, what happens a library is compatible with 8.13.0 and not 8.13-beta1, and does that change by moving packages?
Paolo Giarrusso (Dec 19 2020 at 13:53):But maybe you’re right that it doesn’t change.
Enrico Tassi (Dec 19 2020 at 13:53):Yes, it is up to the coq devs to have good compat records between Xbeta and X. This commitment is why I think we should call it Xrc.
So far, for 8.13, I think I can just move the packages as they are.
Paolo Giarrusso (Dec 19 2020 at 13:55):“Whether the two are compatible” seems intertwined with the other topic. “It doesn’t matter because you don’t see the difference” might be independent.
Paolo Giarrusso (Dec 19 2020 at 13:55):And I think you’re right: if you do have core-dev, you already need special care to avoid the beta, and opam already thinks it’s compatible with your library.
Paolo Giarrusso (Dec 19 2020 at 13:55):If you _don’t_, the beta is not installable, and we _hope_ this doesn’t confuse opam.
Paolo Giarrusso (Dec 19 2020 at 13:57):The only question left is whether we trust opam — I don’t, given all the bugs I’ve seen, but I don’t know what happens here, so up to you.
Enrico Tassi (Dec 19 2020 at 13:57):OK, I think my proposal is more clear now.
And I'm fine if we don't change any "opam layout" until we are all OK that it won't cause breakage on the user's side (which implies good compat records between beta/rc and final).
Enrico Tassi (Dec 19 2020 at 14:00):Paolo Giarrusso said:
The only question left is whether we trust opam — I don’t, given all the bugs I’ve seen, but I don’t know what happens here, so up to you.
Apparently, this is what they do for beta releases of the ocaml compiler. But yes, nobody fully trusts constraint solvers ;-)
Last updated: Jun 03 2023 at 05:01 UTC