Théo Zimmermann (Jun 30 2023 at 14:15): Théo Zimmermann (Jun 30 2023 at 14:15):Emilio Jesús Gallego Arias said:
Moreover we have had this discussion more than twice already, including a call when the solution was decided.
This is true that we had this discussion in a call and that the solution was decided, but the fact that I had completely forgotten about it before you reminded it today and that we are having this discussion again makes me think there should have been a CEP for this (just like there was one for the switch from beta to rc). This would have provided a written record of the pros and cons and the alternatives, and this would have settled things for good.
But I consider Karl an informed observer; if the discussion keeps coming up, maybe the answer isn't sufficiently documented? If it were, questions could be answered by a link.
Exactly! If there had been a CEP, then there would be a link.
Notification Bot (Jun 30 2023 at 14:26):93 messages were moved here from #Coq devs & plugin devs > Coq 8.17.1 by Théo Zimmermann.
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:02):Thanks for moving the thread @Théo Zimmermann , I wanted to do it but had to take off.
There will be a CEP / documentation about that, but here a few incorrect things have been stated, and I think we need to be more careful about asserting factually incorrect things, mainly to use our time properly. In particular, the two main factually incorrect points have been:
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:02):Karl Palmskog said:
my bottom line is that repo activation would be my preferred option for RCs in any opam version, and I have no idea how
avoid-versionwill work out in practice
Ok you don't have an idea, but me and the OCaml maintainers do.
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:03):And so far you have failed to provide any support for your fears, instead you demanded us "proof", I insist this is not a healthy communication practice, the burden of proof is on the person critizicing in this case.
I did detail in past discussions all the problems that the opam 2.0 approach had, so this is not a matter of preferences, but a technical choice with implications.
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:04):Karl Palmskog said:
yeah, I hope there will be some analysis of these commands in many opam versions before they [the instructions] go public
What does that mean?
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:06):Paolo Giarrusso said:
IIUC,
opam switch create 5.1.0~alpha1would fail-safe for opam 2.0. The only downside might be a bad error message?
Yup for opam 2.0 if you do that it will tell you that you need the package that is in the special repos.
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:06):Anyways the users installing rc versions are usually advanced users
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:07):So it is reasonable to expect they read the install guide in the release notes
Emilio Jesús Gallego Arias (Jun 30 2023 at 16:07):Paolo Giarrusso said:
IIUC, that'd require more complex commands for opam >= 2.1, and the upside would be saving
opam --version?
Yes, the recommended command adds a repo that is not needed in newer opam, expert users can just drop that part.
Last updated: Nov 29 2023 at 21:01 UTC