Paolo Giarrusso (Nov 10 2021 at 15:32): Paolo Giarrusso (Nov 10 2021 at 15:32):@Michael Soegtrop that seems to mean that opam upgrade is unsafe on the platform?
Michael Soegtrop (Nov 10 2021 at 16:24):@Paolo Giarrusso : the docs (README / Maintaining an installation) say that one shouldn't call opam upgrade on a platform switch - one should create a new platform switch instead.
But it shouldn't be harmful. E.g. CompCert requires Flocq versions <4 and there is no CompCert which doesn't. So there is no solution to upgrading a Coq Platform installation to Flocq 4.
I intentionally don't pin packages so that people can upgrade individual packages with a few dependencies where it makes sense without unpinning the dependencies.
Paolo Giarrusso (Nov 10 2021 at 18:16):I didn't report it and it might be fixed, but I once thought that opam uninstall foo-X; opam install foo-X would be idempotent, and it turned out not to be — so I lost hope.
Paolo Giarrusso (Nov 10 2021 at 18:19):But it shouldn't be harmful. E.g. CompCert requires Flocq versions <4 and there is no CompCert which doesn't. So there is no solution to upgrading a Coq Platform installation to Flocq 4.
I guess the assumption is that opam upgrade will not uninstall compcert. I think that's reasonable, I just wonder whether it's actually guaranteed.
Michael Soegtrop (Nov 10 2021 at 19:06):My experience is that upgrades and installs fail if there is no solution which keeps all packages. I haven't seen that upgrade or install uninstall packages - unless opam tries to uninstall a new version and this fails.
But again "opam upgrade" is not really in line with the concept of Coq platform.
Paolo Giarrusso (Nov 10 2021 at 20:47):Agree, the only use-case is if you have other packages in the switch (say, dune, merlin, whatever).
Paolo Giarrusso (Nov 10 2021 at 20:50):mostly it's up to preferences and your choice makes sense; I guess this scenario is the only technical question. Is there's a good way to mix switches? Or I guess one should just review opam upgrade's suggestions and do them by hand (which I honestly prefer anyway).
Notification Bot (Nov 11 2021 at 15:42):This topic was moved here from #Coq devs & plugin devs > opam upgrade in the Coq Platform by Théo Zimmermann
Michael Soegtrop (Nov 11 2021 at 16:20):@Paolo Giarrusso :
Paolo Giarrusso said:
Is there's a good way to mix switches?
Well I simply use them in parallel. I have quite a few Coq Platform switches active and switch between them if I want to investigate some different behavior between versions. I would say this is the most useful thing to do. I would change a Coq Platform switch only if this required for specific work. And then I create a new version file, so that I can share this configuration with colleagues. I tend to call "opam install" mostly via the Coq Platform scripts - edit a version file and rerun the platform script with this version file.
Paolo Giarrusso (Nov 11 2021 at 19:08):I mean, in which switch do you install ocaml software? All of them?
Paolo Giarrusso (Nov 11 2021 at 19:08):I guess not
Paolo Giarrusso (Nov 11 2021 at 19:10):in fact, since I use dune I’d probably reinstall dune in each switch (Emilio mentioned a hack the other day but I’ll ignore it for this discussion).
Paolo Giarrusso (Nov 11 2021 at 19:12):I guess my real point is that I’m going to have other software, for which opam upgrade might be reasonable, and that I need to install in my switch next to the Coq platform, and this seems pretty hard to avoid.
Paolo Giarrusso (Nov 11 2021 at 19:14):anyway, these are all hypotheticals, so for once we can defer this discussion until if and when this problem becomes concrete.
Théo Zimmermann (Nov 12 2021 at 13:33):Isn't Dune already installed by the platform?
Michael Soegtrop (Nov 12 2021 at 16:42):Isn't Dune already installed by the platform?
Yes, since some packages depend on it.
Regarding the update question: I think time will show what makes sense. Most people should be able to keep the platform stable for 6 months (intended release schedule).
Last updated: Jun 03 2023 at 05:01 UTC