Stream: Coq devs & plugin devs

Topic: Dynlink error: no implementation available for Tacentries


view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 15:20):

Does anyone understand why open Ltac_plugin is needed inside plugins? If you do not write it, the plugin compiles just fine, but it then fails at execution with Dynlink error: no implementation available for Tacentries. I had forgotten about it and I just wasted two hours rediscovering this issue the hard way.

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

Story is a bit long, and related on how the make-based system builds packed modules (some discussion is at https://github.com/coq/coq/issues/11221 but still confusing)

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

Indeed it is a bug that the current make-based system let's you refer to Tacentries as just a top-level module name, the dune-based build for example does enforce you to use the correct module name Ltac_plugin.Tacentries

view this post on Zulip Emilio Jesús Gallego Arias (Feb 01 2021 at 15:30):

-pack upstream is considered kind of deprecated since the introduction of module aliases, however there was some recent discussion upstream about making it useful again, not sure what will happen.

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 15:36):

I don't understand. If the module is compiled with -for-pack Ltac_plugin, then it is actually called Ltac_plugin.Tacentries, so there is no issue finding it. Or are you saying that Coq does not compile its plugins with -for-pack?

view this post on Zulip Gaëtan Gilbert (Feb 01 2021 at 15:47):

the problem is that unqualfied Tacentries is also found

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 15:49):

But it is not unqualified, due to -for-pack. That is the only job of -for-pack and hopefully it does it right.

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 15:52):

Let me expand: tacinterp.cmi provides a module Ltac_plugin.Tacinterp (due to -for-pack). Coq provides at runtime a module Ltac_plugin.Tacinterp. So, why is Dynlink looking for a module Tacinterp, which has never even existed in the first place?

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 15:53):

Sorry, Tacentries instead of Tacinterp.

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 16:02):

Okay, forget about that. I went and looked at the code of the compiler. Option -for-pack is actually a nop. (The only thing it does is rename constructors of extensible datatypes.) It does not touch modules at all. I wonder why people ever used this option. This explains the issue.

view this post on Zulip Enrico Tassi (Feb 01 2021 at 16:28):

I think that you have to use -for-pack if you want to pack. What is broken is that the .cmi are "found" in their unqualified form (I guess dune does a lot of work behind the scenes to hide the unqualified cmi).

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 17:14):

I just tried. Compiling without -for-pack works fine for bytecode compilation, but not for native compilation. It is when generating the assembly code that the failure happens. And it is only for PowerPC that the generated assembly code is different with -for-pack, but I suppose that the OCaml people wanted the failure to always happen, for portability reasons. (That said, I don't understand why -for-pack causes an extra instruction on PowerPC.)

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 17:16):

As the documentation states, "you can still pack a module that was compiled without -for-pack".

view this post on Zulip Enrico Tassi (Feb 01 2021 at 17:43):

I'm not so sure I follow. IMO your problem is that what happens at compile is not related to what happens at dynload time. tactinterp.cmi (or .cmo) should not morally be around, since they are not linked (their packed version is, as a submodule of Ltac_plugin).

It's not different than dropping a random foo.cmo in your sources and mentioning it in yourplugin.ml. If you then load your code in Coq, dynlink will not found Foo.

-pack should morally remove from the disk the files that were put in the pack (eg tacinterp.cm*), but this is simplistic, since it would trick the build system. A better way would be to build files to pack in a special directory, and only expose the packed result to the rest of the compilation process (dune does this, IMO).

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 17:58):

First, -pack does not have to remove anything; it is the job of the installer to not install useless files. Second, it is not a random foo.cmo; it is one that is linked to Coq and thus should be available to dynamically loaded plugins.

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 18:08):

Let me say it otherwise. If you run ocamlobjinfo on tacinterp.cmx, you will see that it provides Ltac_plugin__Tacentries. And if you run it on ltac_plugin.cmx, you will see that it also provides Ltac_plugin__Tacentries (among others). There is no discrepancy here. The module is available for the plugin, it is just not found.

view this post on Zulip Gaëtan Gilbert (Feb 01 2021 at 18:29):

tacinterp provides tacentries?

view this post on Zulip Guillaume Melquiond (Feb 01 2021 at 18:30):

Damn, again. So, as before, s/tacinterp/tacentries/.

view this post on Zulip Enrico Tassi (Feb 01 2021 at 20:54):

What I think is a bug is that, say, open Tacinterp make ocamlc load tacinterp.cmi but it should not, you should get an error there, since tacinterp.cm* is morally named ltac_plugin__Tacinterp.cm* (so it should not be found). Or at least, this is my mental model of -pack.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2021 at 23:21):

Yeah, current use of pack is a bit problematic and as of today is considered deprecated in favor of aliases [unless some changes upstream happen] , I guess you explained the problems quite well. Coq uses -pack as it was the standard stuff when Pierre did it.


Last updated: Oct 16 2021 at 03:02 UTC