Stream: Coq Platform devs & users

Topic: Strange opam effect


view this post on Zulip Michael Soegtrop (Nov 15 2021 at 10:55):

@Karl Palmskog (and other opam pros), @Enrico Tassi : I see a strange effect in a new pick for 8.13.2:

  - upgrade   ppxlib                   0.15.0 to 0.23.0 [required by elpi]
  - install   elpi                     1.13.7           [required by coq-elpi]

but opam show elpi.1.13.7 gives:

"ppxlib" {>= "0.12.0"}

Why would opam upgrade ppxlib in this situation (which is a problem because serapi requires <= 0.15).

view this post on Zulip Karl Palmskog (Nov 15 2021 at 10:57):

hmm, isn't this just opam trying to use the "latest" ppxlib on an installation?

view this post on Zulip Karl Palmskog (Nov 15 2021 at 10:57):

if one wants to stay on ppxlib 0.15.0, it should be pinned

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 11:06):

I don't pin it by explicitly install ppxlib 0.15.0 before I install elpi and usually opam doesn't upgrade already installed packages unless it must.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 11:14):

I tried the following:

result: opam wants to upgrade Coq to 8.14.0 in the switch, even though there is a version of coq-equations for 8.13.

I think this is the same kind of "upgrade-proneness" as above.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:23):

That's a big problem with ppxlib, ppx_import should be close to solve this issue, but meanwhile you are indeed stuck with old ppxlib for serapi

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:23):

which is a problem for some other packages

view this post on Zulip Karl Palmskog (Nov 15 2021 at 11:24):

so isn't pinning ppxlib to 0.15.0 the recommended way to do this then?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:24):

Newest elpi won't work with 0.15.0

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:25):

Actually that was maybe bad practice they didn't rename ppxlib to ppxlib2 so they could coexist

view this post on Zulip Karl Palmskog (Nov 15 2021 at 11:25):

but that's not what the package for elpi says, as per above it has for ppxlib:>= 0.12.0

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:26):

oh sorry, I assumed elpi was pulling it

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:26):

let me see what pulls it in

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:27):

Note this https://github.com/ocaml-ppx/ppx_import/pull/54 which should help, also we are considering migrating serapi to a different infra

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:28):

Umm, nothing should pull newer ppxlib indeed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 11:28):

need more info like opam list

view this post on Zulip Enrico Tassi (Nov 15 2021 at 11:50):

It may be the dependency on ppx_deriving: https://github.com/LPCIC/elpi/blob/2134e1d5930cb795feddfd606a0e37185a3a6933/elpi.opam#L16-L26

view this post on Zulip Enrico Tassi (Nov 15 2021 at 11:50):

(didn't check, but it may require higher ppxlib)

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:16):

@Karl Palmskog : maybe you are right and opam always updates, although I would find this quite strange. I usually install Coq Platform all packages in parallel, but for debugging "no solution" issues I do it sequentially. If opam indeed updates all dependencies on the go, a sequential build would have a different end result and also take quite a while. I will investigate.

Are there objections against pinning all packages in Coq Platform? I don't like to do this, because it makes it hard to update some packages, also because the opam error messages are not that helpful. If everything is pinned, it is very hard to find out why something can't be installed.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:17):

yeah I don't think it's a good idea to pin everything. Isn't it better to have some kind of documented "pin list"?

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:18):

I'm pretty sure a sequential vs. all-at-once build could have different results. At the very least, the trace will be different, since at first ppxlib 0.23 was OK, but then we get to SerAPI which downgrades to 0.15

view this post on Zulip Enrico Tassi (Nov 15 2021 at 12:21):

I'm for pinning as well.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 12:32):

@Enrico Tassi are you for pinning everything or for pinning selectively like I proposed?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:32):

I'd suggest you folks use opam lock files instead of pinning

view this post on Zulip Enrico Tassi (Nov 15 2021 at 12:33):

Hum, with pinning I meant "selecting a version", sorry for the confusion

view this post on Zulip Enrico Tassi (Nov 15 2021 at 12:33):

all packages are already p.version, but not their dependencies

view this post on Zulip Enrico Tassi (Nov 15 2021 at 12:34):

I'd add to the PACKAGES variable also ppxlib.0.15.0

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

Emilio Jesús Gallego Arias said:

I'd suggest you folks use opam lock files instead of pinning

That's actually a pretty good suggestion! But will it keep working with opam 2.0 or do we need opam 2.1 for this?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:36):

@Théo Zimmermann opam 2.1 is needed, but for a setup such as the one in the platfrom I don't see trouble moving to 2.1, in fact it should be recommeneded to do so, 2.1 is a fine version of opam

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

Sure, I guess if opam is not installed, the platform installs opam 2.1, but it also works with an existing opam installation, so this means that we would need to check what version is installed and upgrade or fail in case it is opam 2.0.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:41):

I don't see a lot of trouble asking people to go to 2.1

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

it is not like the 1 -> 2 migration, that was a major upgrade

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

this is a 2.x release, so almost everything works out of the box

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

except in a very few corner cases regading depext

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

but that, 2.1 should be much better I understand

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:43):

one choice if opam 2.0 is present, is to work without the lock file, actually you can simulate it, from the lock file you can generate an opam install foo.x.y.z bar.x.y.z ..... moo.x.y.z line, but likely not worth it

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:43):

@Karl Palmskog, @Enrico Tassi : yes, I changed the package lists such that ppxlinb.0.15 is installed upfront. I still have the issue that when opam comes to elpi, it want's to update ppxlib, so I guess I need to pin ppxlib.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:44):

Moreover opam 2.1 is more stable w.r.t. dep resolution

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:45):

But we are in a bit of mess unfortunately due to the ppx situation, plus the 4.08 plugins situation

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:45):

Regarding the opam version: if we require 2.1 I would change the platform scripts such that they update automatically to 2.1 after asking the user. I learned the hard way that updating opam is not that trivial - after updating the opam executable one has to run some extra commands to update stuff like the sandbox scripts.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:46):

@Michael Soegtrop indeed auto-updating opam would be a bit too much

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:46):

IMHO we should ask the user to do that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:46):

the 4.08 plugins situation has a potential to create a huge mess :S :S

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:47):

for example the moment math-comp uses HB

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:47):

and the platform expands a bit, we are gonna do boom

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:48):

@Emilio Jesús Gallego Arias : as I said - I would ask the user first and in my experience it is not rare that users end up with half way in between opam setups if they do it manually.

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:49):

@Emilio Jesús Gallego Arias: what is the 4.08 plugin situation? And what is the issue with HB (beyond elpi + ppxlib)?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:49):

@Michael Soegtrop see https://github.com/coq/coq/issues/12067

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:50):

And what would be the advantage of a lock file vs. pinning? Wouldn't users still have a very hard time to install additional packages which require updates for some packages?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:50):

Basically all plugins linking some external OCaml lib are incompatible with each other for OCaml >= 4.08

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:50):

that includes elpi, serapi, Talia's stuff, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:51):

Michael Soegtrop said:

And what would be the advantage of a lock file vs. pinning? Wouldn't users still have a very hard time to install additional packages which require updates for some packages?

A lock file is a way to let the package help with the pinnings

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:51):

tends to be pretty convenient

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 12:52):

there are also some internal details, as pinning has a bit of different semantics in OPAM , but not too relevant

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:53):

Regarding lock files / pinning: I still think one should lock/pin is little as possible to keep things flexible. The main issue is that opam produces 0 helpful messages if packages have incompatibilities and everything is pinned.

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 12:54):

Regarding link issues: so should I go back to Ocaml 4.07 with Coq Platform? I recently updated to 4.10.2. I test all plugins, but not two plugins together.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 13:00):

Going back to 4.07 is a short-term fix only, the issue needs to be fixed properly.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 13:00):

I am not expert but i think there is significant evidence pointing in the other direction wrt lock files,

view this post on Zulip Enrico Tassi (Nov 15 2021 at 13:36):

Michael Soegtrop said:

Karl Palmskog, Enrico Tassi : yes, I changed the package lists such that ppxlinb.0.15 is installed upfront. I still have the issue that when opam comes to elpi, it want's to update ppxlib, so I guess I need to pin ppxlib.

I didn't look at the scripts later, but if you do opam install x.v1; opam install y.v2 then it could happen, but if you do opam install x.v1; opam install x.v1 y.v2 then it should not. Would it be possible to "pair" elpi and serapi with ppxlib in their installation command?

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 13:47):

@Enrico Tassi : I will do some more tests. Currently it is either all sequential or all parallel, but one could implement package groups" in case this is required.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 13:51):

most pure Coq projects are very predictable, but any plugin or OCaml tool typically has a bunch of high-velocity dependencies. I think it might make sense to have one group for OCaml-plugins-or-tools, and then the rest should be installable sequentially or in parallel, doesn't matter...

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 13:56):

My current plan is to pin a minimal number of packages, so that I get the same result in parallel and sequential builds and no rebuilds in the sequential build. It might be only ppxlib, because afik it is the only OCaml package for which we have an upper bound.

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 14:12):

It would be sufficient to pin packages only in a sequential build. Should I also pin in parallel builds - I would do this after the parallel install then.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:36):

@Michael Soegtrop About using opam lock, I don't have experience with it, so it is possible that some of what I say isn't fully correct, but from my understanding this is not comparable to pinning, and therefore should not be dismissed so fast as it might provide a real solution to the problem you are facing, without involving pinning.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:37):

IIUC opam lock is about making an installation reproducible. This is exactly what we want to do with the platform.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:37):

Basically, you would create once an opam switch which corresponds to a platform variant and then generate the lock for it.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:38):

Then, installing the platform switch would just amount to running install on the lockfile.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:39):

Once again, to the best of my limited understanding, this would install packages without pinning them, so this would keep the properties you wanted for the platform switches.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:39):

On the other hand, this would guarantee that you get the exact same versions installed in every platform switch of a given variant.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:39):

And it also has the potential of significantly reducing the complexity of the platform scripts...

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:41):

my experience with lock files in Ruby was that one constantly has to regenerate them to keep up-to-date for packages with dependencies that change often.

view this post on Zulip Enrico Tassi (Nov 15 2021 at 14:42):

the same happens in javascript, but bots help you there

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:43):

good point about JavaScript. So if there is some tooling to help out with updating the lock files, then it could work out, but manual lockfile management can turn into a ton of work.

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:44):

Sure, but there are two differences that matter here:

view this post on Zulip Théo Zimmermann (Nov 15 2021 at 14:44):

What is the issue with having to regenerate the lock file before each new platform release?

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 15:01):

OK, I will look into the lock files - not sure how one would do a sequential build with this method and still be flexible afterwards, but maybe it works.

I guess the issue with regenerating was meant in case one has to regenerate it while a release should be stable.

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

seems the lock file should come with the release?

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 15:03):

But for the time being I will use pinning - it is only ppxlib.

Again the question; should I also pin it in a parallel build, where this is not strictly required?


Last updated: Jan 30 2023 at 11:03 UTC