Shachar Itzhaky (Nov 15 2020 at 11:23): Shachar Itzhaky (Nov 15 2020 at 11:23):Hi guys,
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?
Enrico Tassi (Nov 15 2020 at 12:57):Hum, no, I never really understood what was wrong.
Emilio Jesús Gallego Arias (Nov 15 2020 at 14:54):@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.
Shachar Itzhaky (Nov 15 2020 at 15:33):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.
Emilio Jesús Gallego Arias (Nov 15 2020 at 15:49):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:
Emilio Jesús Gallego Arias (Nov 15 2020 at 15:49):ocamlobjinfo elpi_plugin.cma | grep 'unsafe features: YES'
Uses unsafe features: YES
Uses unsafe features: YES
which seems to come from camlp5
Shachar Itzhaky (Nov 16 2020 at 08:05):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).
Emilio Jesús Gallego Arias (Nov 16 2020 at 16:41):I guess you disabling the safe check should work, given the code in camlp5
Emilio Jesús Gallego Arias (Nov 16 2020 at 16:42):There is a function in the Dynlink API
Last updated: Jun 04 2023 at 22:30 UTC