Stream: jsCoq

Topic: Dynlink error (unsafe features)


view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 15 2020 at 12:57):

Hum, no, I never really understood what was wrong.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2020 at 15:50):

which seems to come from camlp5

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2020 at 16:42):

There is a function in the Dynlink API


Last updated: Jan 31 2023 at 09:01 UTC