While fiddling with waCoq (jsCoq's WebAssembly sibling) I encountered this old error situation upon trying to load elpi:
[Loading ML file elpi_plugin.cma ... failed] Dynlink error: this object file uses unsafe features
I noticed that @Enrico Tassi and @Emilio Jesús Gallego Arias have been part of a discussion on this matter some time ago (Aug 2019). How did you solve it at the time?
Hum, no, I never really understood what was wrong.
@Shachar Itzhaky this is usually raised when then dynlinked module contains C-level primitives, you can try to call
Dynlink.allow_unsafe_modules but somehow you will have to provide the right stubs too.
Curious, from looking at the sources of the elpi plugin, it seems that it only has OCaml source files. Also, when a C primitive is missing,
ocamlrun typically says something like
missing primitive unix_stat; but perhaps that is not the behavior when the object is loaded with Dynlink.
Note that elpi is built using linkall [which is a critical bug in itself], so indeed you need to account for all transitive deps, a quick look reveals:
ocamlobjinfo elpi_plugin.cma | grep 'unsafe features: YES' Uses unsafe features: YES Uses unsafe features: YES
which seems to come from camlp5
Thanks @Emilio Jesús Gallego Arias ! I assume it needs
linkall because it links with elpi 1.11. We had this discussion before; if a plugin needs a library that is not linked to coqtop, then
linkall is the only available avenue right now. I will see what can be done w.r.t. loading unsafe objects (in jsCoq, Dynlink does not check this ofc, and elpi seems to load ok, although I haven't tried running anything fancy).
I guess you disabling the safe check should work, given the code in camlp5
There is a function in the Dynlink API
Last updated: Jan 31 2023 at 09:01 UTC