Stream: Coq Platform devs & users

Topic: Strange opam effect

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).

Karl Palmskog (Nov 15 2021 at 10:57):

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

Karl Palmskog (Nov 15 2021 at 10:57):

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

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.

Karl Palmskog (Nov 15 2021 at 11:14):

I tried the following:

• unpin Coq 8.13 in one of my switches
• do opam install coq-equations

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.

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 11:23):

which is a problem for some other packages

Karl Palmskog (Nov 15 2021 at 11:24):

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 11:24):

Newest elpi won't work with 0.15.0

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

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 11:26):

oh sorry, I assumed elpi was pulling it

Emilio Jesús Gallego Arias (Nov 15 2021 at 11:26):

let me see what pulls it in

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 11:28):

Umm, nothing should pull newer ppxlib indeed

Emilio Jesús Gallego Arias (Nov 15 2021 at 11:28):

need more info like opam list

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

Enrico Tassi (Nov 15 2021 at 11:50):

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

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.

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"?

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

Enrico Tassi (Nov 15 2021 at 12:21):

I'm for pinning as well.

Karl Palmskog (Nov 15 2021 at 12:32):

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:32):

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

Enrico Tassi (Nov 15 2021 at 12:33):

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

Enrico Tassi (Nov 15 2021 at 12:33):

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

Enrico Tassi (Nov 15 2021 at 12:34):

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

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?

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

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.

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

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

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

except in a very few corner cases regading depext

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:42):

but that, 2.1 should be much better I understand

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

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.

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:44):

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

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

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.

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:46):

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:46):

IMHO we should ask the user to do that

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:47):

for example the moment math-comp uses HB

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:47):

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

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.

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)?

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:49):

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

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?

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:50):

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

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 12:51):

tends to be pretty convenient

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

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.

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.

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.

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,

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?

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.

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...

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.

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.

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.

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.

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.

Théo Zimmermann (Nov 15 2021 at 14:38):

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

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.

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.

Théo Zimmermann (Nov 15 2021 at 14:39):

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

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.

Enrico Tassi (Nov 15 2021 at 14:42):

the same happens in javascript, but bots help you there

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.

Théo Zimmermann (Nov 15 2021 at 14:44):

Sure, but there are two differences that matter here:

• first, fortunately the Coq and even the OCaml ecosystems are smaller and evolve more slowly
• second, the goal of the platform is reproducibility first and foremost, so a given release should have a given pick of all packages, and should not move as soon as a dependency is updated.

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?

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.

Paolo Giarrusso (Nov 15 2021 at 15:02):

seems the lock file should come with the release?

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: Jun 03 2023 at 03:01 UTC