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
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)
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.
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?
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.
Is this related to https://github.com/coq/coq/issues/12067 , and is using OCaml 4.07.1 another workaround (like in that issue)?
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.
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…
See https://github.com/ejgallego/coq-serapi/issues/260#issuecomment-951008048
I think "works by accident" [to combine Elpi and SerAPI on 4.07.1] qualifies as a workaround
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
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?
Li-yao has marked this topic as resolved.
Li-yao has marked this topic as unresolved.
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.
if you mean you see the cmxs, findlib won't see it without a meta file
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...
How do I get it to know about that META file?
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.
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"
)
Notice the line directory = "plugin"
.
Ok so it's not confused about the META file? then why the error if the cmxs is right there?
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.
The Lib
module is in Interfaces imported
instead. But the Coqsimpleio_plugin__Lib
object files are also in the same directory.
That is not sufficient. They have to actually be part of the cmxs file.
(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.)
So I have to find a dune incantation to link it properly?
Yes.
@Li-yao does using Declare ML Module "$pkg.findlib_name"
solve your problem?
as of today there is still some compat code, it seems that could be your problem
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
Oh, "$pkg.findlib_name"
does find transitive dependencies, while that backcompat layer doesn't.
Yup, the backcompat layer doesn't call findlib
Someone needs to open a bug in https://github.com/ocaml/dune/issues to track the issue @Enrico Tassi mentioned.
Li-yao has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC