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 Ltac_plugin.Tacentries
-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 -for-pack
?
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?
Sorry, Tacentries
instead of Tacinterp
.
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 -for-pack
".
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).
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.
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.
tacinterp provides tacentries?
Damn, again. So, as before, s/tacinterp/tacentries/
.
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: Oct 13 2024 at 01:02 UTC