Stream: Coq devs & plugin devs

Topic: ✔ Plugins with shared code


view this post on Zulip Li-yao (Apr 10 2022 at 04:12):

I'm trying to make two plugins share some code but I keep running into weird behaviors. I have a minimal example here https://github.com/Lysxia/plugin-hell-please-ignore

  1. I can't build the second plugin (which depends on code from the first) using coq_makefile

    Dynlink error: The module `Coq_config' is already loaded (either by the main program or a previously-dynlinked library)
    
  2. Using Dune instead, I can only load the second plugin (Declare ML Module) in its .v module after importing the first plugin (From One Import One.), because that somehow helps coq find where the .ml module shared between both plugins is.

  3. In that example, the "shared module" is bundled with the first plugin. I've also tried pulling it into its own dune library, in a different subdirectory of the first plugin, but then the Declare ML Module vernac of that first plugin fails because it lost track of that separated module, I guess for a similar reason to (2).

What am I doing wrong?

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 07:18):

As you noticed, OCaml's dynamic loader refuses to load two modules with the same name, and it does not transitively load shared libraries either. So, a first solution is to have three Coq plugins, the first one bundling the shared code. A second solution is to use Coq's master branch, as it no longer directly calls OCaml's dynamic loader but instead calls the Findlib wrapper. That makes it possible to have transitive dependencies, at the expense of putting meta files (aptly named META) all over the place.

view this post on Zulip Paolo Giarrusso (Apr 10 2022 at 07:24):

Is this related to https://github.com/coq/coq/issues/12067 , and is using OCaml 4.07.1 another workaround (like in that issue)?

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 07:38):

No, it won't help. The bug report fails to mention a critical point: it is the Num library that is doubly linked. So, using an old version of OCaml only works by accident, because Num was not a shared library at the time, so no shared library means no dynamic linking.

view this post on Zulip Paolo Giarrusso (Apr 10 2022 at 08:47):

While I don’t have the full picture, I think we run elpi and alectryon using together using OCaml 4.07.1 exactly for this reason, and they share a different library…

view this post on Zulip Paolo Giarrusso (Apr 10 2022 at 08:49):

See https://github.com/ejgallego/coq-serapi/issues/260#issuecomment-951008048

view this post on Zulip Karl Palmskog (Apr 10 2022 at 08:53):

I think "works by accident" [to combine Elpi and SerAPI on 4.07.1] qualifies as a workaround

view this post on Zulip Karl Palmskog (Apr 10 2022 at 08:57):

but as Guillaume says, Elpi+SerAPI (and other problematic plugin combinations) on OCaml >= 4.08 will be solved in 8.16.0, since we have META all over the place. coq_makefile will generate the boilerplate with directives like these

view this post on Zulip Gaëtan Gilbert (Apr 10 2022 at 09:08):

Guillaume Melquiond said:

No, it won't help. The bug report fails to mention a critical point: it is the Num library that is doubly linked. So, using an old version of OCaml only works by accident, because Num was not a shared library at the time, so no shared library means no dynamic linking.

Isn't it because <4.08 doesn't error on double linking?

view this post on Zulip Notification Bot (Apr 10 2022 at 12:25):

Li-yao has marked this topic as resolved.

view this post on Zulip Notification Bot (Apr 10 2022 at 15:09):

Li-yao has marked this topic as unresolved.

view this post on Zulip Li-yao (Apr 10 2022 at 15:14):

Thanks for the info!

So I'm now trying the master branch, and IIUC I wouldn't need to add spurious imports to load transitive dependencies, but I'm actually still getting dynlink errors. What's puzzling is also, in the findlib paths listed by the error message, I can see the location of the dependency right there.

view this post on Zulip Gaëtan Gilbert (Apr 10 2022 at 15:18):

if you mean you see the cmxs, findlib won't see it without a meta file

view this post on Zulip Li-yao (Apr 10 2022 at 15:18):

Ah, actually the error lists .opam/my-switch/lib/mypackage/plugin but not .opam/my-switch/lib/mypackage, which is where the META file is...

view this post on Zulip Li-yao (Apr 10 2022 at 15:20):

How do I get it to know about that META file?

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 15:33):

What is the actual error? In particular, are you sure it isn't complaining about the location of the plugin rather than the location of the META file? In which case, you need to review the content of your META file.

view this post on Zulip Li-yao (Apr 10 2022 at 15:38):

I'm not sure, but the error message is:

File "./src/QuickChick_Plugin.v", line 1, characters 0-60:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/sam/code/coq/QuickChick/_build/default/plugin/quickchick_plugin.cmxs: undefined symbol: camlCoqsimpleio_plugin__Lib\")")
Findlib paths:
...
/home/sam/.opam/coq-dev/lib/coq-simple-io/plugin
cat ~/.opam/coq-dev/lib/coq-simple-io/META
package "plugin" (
  directory = "plugin"
  version = "6dd39ae"
  description = ""
  requires = "coq-core.plugins.extraction unix"
  archive(byte) = "coqsimpleio_plugin.cma"
  archive(native) = "coqsimpleio_plugin.cmxa"
  plugin(byte) = "coqsimpleio_plugin.cma"
  plugin(native) = "coqsimpleio_plugin.cmxs"
)

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 15:45):

Notice the line directory = "plugin".

view this post on Zulip Li-yao (Apr 10 2022 at 16:04):

Ok so it's not confused about the META file? then why the error if the cmxs is right there?

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 16:15):

Make sure your plugin actually contains a Lib module. You can use ocamlobjinfo ~/.opam/coq-dev/lib/coq-simple-io/plugin/coqsimpleio_plugin.cmxs and look into the "Globals defined" section.

view this post on Zulip Li-yao (Apr 10 2022 at 16:19):

The Lib module is in Interfaces imported instead. But the Coqsimpleio_plugin__Lib object files are also in the same directory.

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 16:22):

That is not sufficient. They have to actually be part of the cmxs file.

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 16:26):

(You can make them part of a different cmxs file, but then you need to add a requires line to your plugin, so that that other cmxs file is loaded beforehand.)

view this post on Zulip Li-yao (Apr 10 2022 at 16:28):

So I have to find a dune incantation to link it properly?

view this post on Zulip Guillaume Melquiond (Apr 10 2022 at 16:28):

Yes.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2022 at 13:08):

@Li-yao does using Declare ML Module "$pkg.findlib_name" solve your problem?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2022 at 13:08):

as of today there is still some compat code, it seems that could be your problem

view this post on Zulip Enrico Tassi (Apr 11 2022 at 13:22):

If you use dune then you should use the backward compat layer waiting for a release that works with Declare ML Module "$pkg.findlib_name", see for example this commit: https://github.com/damien-pous/relation-algebra/pull/30/commits/1032d73c27f1b883d4387a7d8690e27972cb11f2

view this post on Zulip Li-yao (Apr 11 2022 at 13:28):

Oh, "$pkg.findlib_name" does find transitive dependencies, while that backcompat layer doesn't.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2022 at 13:30):

Yup, the backcompat layer doesn't call findlib

view this post on Zulip Emilio Jesús Gallego Arias (Apr 11 2022 at 13:31):

Someone needs to open a bug in https://github.com/ocaml/dune/issues to track the issue @Enrico Tassi mentioned.

view this post on Zulip Notification Bot (Apr 11 2022 at 13:37):

Li-yao has marked this topic as resolved.


Last updated: Feb 06 2023 at 19:03 UTC