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.
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)
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
-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.
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
the problem is that unqualfied
Tacentries is also found
But it is not unqualified, due to
-for-pack. That is the only job of
-for-pack and hopefully it does it right.
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?
Tacentries instead of
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.
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).
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.)
As the documentation states, "you can still pack a module that was compiled without
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.
.cmo) should not morally be around, since they are not linked (their packed version is, as a submodule of
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
-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).
-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.
Let me say it otherwise. If you run
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.
tacinterp provides tacentries?
Damn, again. So, as before,
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.
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: May 28 2023 at 16:30 UTC