Michael Soegtrop (Nov 15 2021 at 16:59): Michael Soegtrop (Nov 15 2021 at 16:59):@Emilio Jesús Gallego Arias mentioned above that Coq plugins are essentially broken with Ocaml >= 4.08. I recently switched to 4.10.2 and now wonder if this was smart. Afaik everything in Coq Platform 2021.11 still works with 4.07 (the version used in 2021.02). The only issue I know of is that Apple silicon Macs require OCaml >= 4.10.2, but one could make this platform dependent.
Enrico Tassi (Nov 15 2021 at 17:14):the only problem I'm aware of is loading elpi and serapi. imo the problem is minor for this platform. said that, we should try to address it in coq by loading plugins via findlib.
Paolo Giarrusso (Nov 15 2021 at 20:52):aka, serapi is busted on M1? :-(. But I agree that’s not super-urgent.
Paolo Giarrusso (Nov 15 2021 at 20:53):OTOH I hope to use elpi and M1 soon (of course Rosetta is a good work around)
Théo Zimmermann (Nov 15 2021 at 21:00):No, there is no issue with SerAPI alone on recent OCaml versions. The issues are rather when loading several plugins which link to the same OCaml dependencies.
Théo Zimmermann (Nov 15 2021 at 21:00):Recent discussions about this happened in: https://github.com/coq/coq/issues/14260
Paolo Giarrusso (Nov 15 2021 at 21:38):Oh, it's https://github.com/ejgallego/coq-serapi/issues/260
Paolo Giarrusso (Nov 15 2021 at 21:46):Thanks for the link, so I can plan ahead!
Michael Soegtrop (Nov 16 2021 at 08:56):Thanks for the comments! So I will stay with 4.10.2 and see what happens.
Emilio Jesús Gallego Arias (Nov 16 2021 at 09:58):Yeah we found SerAPI + HB, but likely many other bad interactions are problematic, for example tactician, most (if not all) Talia's stuff, etc.... the moment people start to use two non-trivial plugins we are gonna find the problem. Thus I disagree with those that state it is a minor issue. It seems very serious to me.
There are workarounds tho, for example it is easy to pin a coq-elpi tree that works with serapi, but at some point you have a diamond and only one load order works :S
As for the platform, I see no reason to use 4.10 instead of 4.12 for example [that assuming the critical bugs of 4.10 were fixed in 4.10.2, I didn't check]
Michael Soegtrop (Nov 16 2021 at 10:48):@Emilio Jesús Gallego Arias : there are certain restrictions on what OCaml versions are available on Windows - if there are good reasons to use 4.12 I can check if it is available.
But if there are serious issues with plugins, and since Coq Platform is especially made to make the use of various plugins easier, wouldn't it be better to go to the latest 4.07 release until this is fixed?
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:06):I dunno, actually the platform only includes two conflict plugins? IMHO we should spend manpower on fixing the issue, it is not hard to fix actually
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:06):I have virtually zero times these days :S
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:06):Trying to find someone who can help with development on my projects :S
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:07):So the issue may not be serious now, but what I mean is that at some point is gonna bit us big, specially if we plan to have many libraries using plugins such as HB
Karl Palmskog (Nov 16 2021 at 11:07):@Michael Soegtrop I think this illustrates that the platform needs not just individual smoke tests, but "combinatorial" smoketests, where plugins are loaded together, possibly in different orders
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:09):We are in deeper trouble with OCaml anyways, AKA OCaml 5.0
Karl Palmskog (Nov 16 2021 at 11:10):but if the switch to 5.0 is a big thing, than that basically means less effort (in the longer run), just make the jump to 5.0 all at once and drop 4.X
Karl Palmskog (Nov 16 2021 at 11:14):Emilio Jesús Gallego Arias said:
So the issue may not be serious now, but what I mean is that at some point is gonna bit us big, specially if we plan to have many libraries using plugins such as HB
since the Platform is about encouraging reuse and getting away from dependency aversion, intra-platform plugin problems should be high priority IMO. Already many MathComp projects are starting to use HB for simple declarations that could be done without it.
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:23):Karl Palmskog said:
but if the switch to 5.0 is a big thing, than that basically means less effort (in the longer run), just make the jump to 5.0 all at once and drop 4.X
We are not compatible with 5.0 and the fix is far from trivial in terms of manpower, maybe we are lucky and some devs invest a large amount of time, but in principle it will be a lot of work we don't have the manpower for
Emilio Jesús Gallego Arias (Nov 16 2021 at 11:23):Karl Palmskog said:
Emilio Jesús Gallego Arias said:
So the issue may not be serious now, but what I mean is that at some point is gonna bit us big, specially if we plan to have many libraries using plugins such as HB
since the Platform is about encouraging reuse and getting away from dependency aversion, intra-platform plugin problems should be high priority IMO. Already many MathComp projects are starting to use HB for simple declarations that could be done without it.
I agree indeed, what we can observe now is not very serious, but the issue is
Michael Soegtrop (Nov 16 2021 at 11:57):@Emilio Jesús Gallego Arias : the packages which are afaik plugins are:
Which of these are affected by the issues I can't tell. I am not sure if lia, zify, nra and so on count as plugins.
How would I know if they work together or not? Would the Require already fail?
Karl Palmskog (Nov 16 2021 at 12:00):technically lia and zify and nra are plugins to my knowledge, but to me they are not the responsibility of the platform
Karl Palmskog (Nov 16 2021 at 12:02):I think currently, the errors will only happen when someone links at the OCaml level to both SerAPI and HB in a certain order (Emilio should confirm). Since SerAPI does not come with a .v file with a Require that loads the OCaml parts, this has to be done manually
Karl Palmskog (Nov 16 2021 at 12:03):the easiest way to trigger it currently may be to use Alectryon on a Coq development that uses HB. Then the Coq file is processed through the sertop OCaml program that uses SerAPI, and at the same time linking with HB via Coq
Paolo Giarrusso (Nov 16 2021 at 13:57):Even just ELPI is enough, which increases impact.
Paolo Giarrusso (Nov 16 2021 at 13:58):Since we use Alectryon and plan to use elpi, my plan here for Bedrock is to keep our CI on 4.07.1+flambda for longer.
Karl Palmskog (Nov 16 2021 at 14:00):well, I think there are very few people that use plain ELPI, but good point, that makes a potential smoke test smaller
Paolo Giarrusso (Nov 16 2021 at 14:12):@Michael Soegtrop anyway, :+1: for an arch-dependent OCaml version, even if sadly the elpi/HB + serapi/alectryon combo is for now busted on M1 :-|
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:43):mtac for example will not pass ci as it depends on unicoq
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:43):if you see the original issue that was the first time we witnessed the probelm
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:44):any two plugins that link statically the same lib will fail, there are already many combos like that
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:45):I don't see a lot of value in trying to discover what combos are broken, that can change quickly and it is not hard to workaroudn
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:45):for example we can patch coq-elpi and serapi so they work together in the platfrom
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:45):instead we should allocate time to fix the root issue
Karl Palmskog (Nov 16 2021 at 14:46):but I think it would be nice to have a smoke test where they do something together if it shows up again in the future
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:46):which should by the way provide a much better experience for people willing to link to external libs
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:46):Karl Palmskog said:
but I think it would be nice to have a smoke test where they do something together if it shows up again in the future
too many combos to test, if people want to do that OK, but that's IMO a loss of time
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:46):the issue is very specific
Emilio Jesús Gallego Arias (Nov 16 2021 at 14:47):we violated the OCaml spec, now we pay for it
Enrico Tassi (Nov 16 2021 at 15:12):Paolo Giarrusso said:
Since we use Alectryon and plan to use elpi, my plan here for Bedrock is to keep our CI on 4.07.1+flambda for longer.
Good to know. I'll then try to fix the issue on the coq side using findlib to load code and try to remove -linkall from makefiles, and see where we go.
Théo Zimmermann (Nov 16 2021 at 15:20):Emilio Jesús Gallego Arias said:
mtac for example will not pass ci as it depends on unicoq
Somehow something made it work, no? (Because it's already included in the Coq platform.)
Enrico Tassi (Nov 16 2021 at 15:21):if unicoq does not link anything extra, then there is no reason for it not to work
Enrico Tassi (Nov 16 2021 at 15:22):in a sense, if all the extra code is already in coq, there will be no "double runtime linking". but if plugin p1 and p2 both depend on lib1 which is not already linked in Coq, boom.
Enrico Tassi (Nov 16 2021 at 15:23):today p1 and p2 are linked with -linkall, so they both "embed" lib1, and that causes the clash. Findlib is a proper runtime liker, it would load first lib1 (once) and then p1 and p2
Théo Zimmermann (Nov 16 2021 at 15:23):There used to be an issue with mtac2 though (IIRC just because of the two plugins having to link with Coq internal plugins like Ltac). Maybe this has been fixed on the Coq-side.
Enrico Tassi (Nov 16 2021 at 15:24):you can pass a blacklist to -linkall
Enrico Tassi (Nov 16 2021 at 15:24):I think that was it
Enrico Tassi (Nov 16 2021 at 15:24):it already existed, but was outdated
Emilio Jesús Gallego Arias (Nov 16 2021 at 15:26):https://github.com/coq/coq/pull/11580 for the mtac2 failure
Emilio Jesús Gallego Arias (Nov 16 2021 at 15:27):Théo Zimmermann said:
Emilio Jesús Gallego Arias said:
mtac for example will not pass ci as it depends on unicoq
Somehow something made it work, no? (Because it's already included in the Coq platform.)
That's why this bug is so tricky, sometimes may trigger, sometimes not, depending on what exact context you load.
Michael Soegtrop (Nov 16 2021 at 16:53):So what is the conclusion? Should I follow @Paolo Giarrusso 's example and stick to 4.07.1 (with or without flambda) - except for Apple silicon which requires OCaml >= 4.10.2?
Or should I stick with 4.10.2?
What tests can I do? Should I require all plugins in plugin smoke test files?
Karl Palmskog (Nov 16 2021 at 16:59):you have conflicting opinions on the test thing: I think it's good to record some basic interactions (e.g., SerAPI/sertop and coq-elpi) if we knew there was a problem, but Emilio thinks it's not worth the trouble.
Karl Palmskog (Nov 16 2021 at 17:00):if I'm reading Enrico right he can release a version of coq-elpi where the problem goes away, but probably not for a while?
Karl Palmskog (Nov 16 2021 at 17:01):I would probably document this as a known issue that rarely gets triggered and stay on OCaml 4.10
Théo Zimmermann (Nov 16 2021 at 17:03):@Enrico Tassi was talking about fixing this the proper way in Coq IIUC.
Karl Palmskog (Nov 16 2021 at 17:04):with the current "conservative" point releases, this is then very unlikely to appear in 8.14
Théo Zimmermann (Nov 16 2021 at 17:05):Impossible in 8.14, unlikely in 8.15.
Karl Palmskog (Nov 16 2021 at 17:06):I'm missing a :despair: emoji...
Théo Zimmermann (Nov 16 2021 at 17:06)::sob:
Karl Palmskog (Nov 16 2021 at 17:07):well, that's a bit different
Théo Zimmermann (Nov 16 2021 at 17:07):Anyway, Emilio has been warning us about this for so long. I'd actually be pretty happy if it was solved in 8.16 once and for all.
Enrico Tassi (Nov 16 2021 at 18:14):@Michael Soegtrop I would just document the problem, that is serapi + elpi don't work (the only use case is running alectryon on code using elpi). In this case, use the platform scripts to pick a different compiler. Maybe we need a flag to stick to 4.07.1.
Enrico Tassi (Nov 16 2021 at 18:15):I would keep the default to be what we used so far, and consider 4.07 a way to work around a known issue.
Paolo Giarrusso (Nov 16 2021 at 18:17):The only hard constraint is to not drop 4.07 yet (from the compilers Coq supports)
Paolo Giarrusso (Nov 16 2021 at 18:19):OCaml-version-while, till a couple of weeks ago all these version were busted on the latest glibc/Ubuntu stable, I’m not sure the OCaml patch was backported yet…
Paolo Giarrusso (Nov 16 2021 at 18:22):indeed — @Michael Soegtrop you’ll need to backport https://github.com/ocaml/opam-repository/pull/19855 if you want to support 21.10, _or_ mark it as unsupported.
Paolo Giarrusso (Nov 16 2021 at 18:24):this argues for sticking to 4.10 + backport (or to an even later OCaml if it works?), because “compile on the latest Ubuntu” is probably much more important than “support this plugin combo”. The MR claims plans to backport to 4.09 and earlier, but says that’s harder, and progress seems slow (it’s also tons of work!)
Michael Soegtrop (Nov 17 2021 at 08:30):So I would say the conclusion is that the platforms script should have a flag to ask advanced questions, one of which would be the OCaml version and we should test if everything compiles with 4.07.1 in CI (I would do it only on Ubuntu then).
Last updated: Jan 30 2023 at 11:03 UTC