Stream: Coq Platform devs & users

Topic: opam upgrade in the Coq Platform


view this post on Zulip Paolo Giarrusso (Nov 10 2021 at 15:32):

@Michael Soegtrop that seems to mean that opam upgrade is unsafe on the platform?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:08):

I mean, in which switch do you install ocaml software? All of them?

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:08):

I guess not

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 12 2021 at 13:33):

Isn't Dune already installed by the platform?

view this post on Zulip 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: Jan 30 2023 at 10:03 UTC