Dnylink Error when trying to add merlin-lib as dependency · Coq devs & plugin devs

I was working on extraction plugin and wanted to use merlin-lib as a dependency. Yet, I encountered a dynlink error when I tried to build dune. There are various discussions on Github but none of them seem to provide any concrete steps to solve the problem. Is there any easy solution to this?

Gaëtan Gilbert (Apr 17 2023 at 16:20):

I think stdlib still uses the legacy (non findlib) plugin loader so no easy solution

Rodolphe Lepigre (Apr 18 2023 at 07:41):

I was about to suggest a workaround (by building a statically linked .cmxs file with dune), which could perhaps be done, but would be super painful given the amount of dependencies that merlin-lib has. I recently did this for a plugin, but the library I was depending on (mtime.clock.os) only depended on one other dependency (mtime). So I could do something like:

(library
 (name my_plugin)
 (public_name my_package.my_plugin)
 (libraries mtime.clock.os))

; FIXME: the following is a big hack.

(rule
 (targets mtime.where)
 (action
  (with-stdout-to %{targets}
   (pipe-stdout
    (run ocamlfind query mtime)
    (run tr -d '\n')))))

(rule
 (targets mtime.clock.os.where)
 (action
  (with-stdout-to %{targets}
   (pipe-stdout
    (run ocamlfind query mtime.clock.os)
    (run tr -d '\n')))))

(rule
 (targets my_plugin_with_deps.cmxs)
 (action
  (run %{ocamlopt} -shared -o %{targets} -linkall
       -I .
       -I %{read:mtime.where}
       -I %{read:mtime.clock.os.where}
    mtime.cmxa
    mtime_clock.cmxa
    %{cmxa:my_plugin})))

When you do that you also need an empty my_plugin_with_deps.mlpack, and also the theory where you load that plugin needs to have some custom (dummy) dune rule depending on the .cmxs and the .mlpack files so that they are produced early enough (I can give more details if anyone cares). And of course, in you need to do Declare ML Module "my_plugin_with_deps:my_package.my_plugin"..

Gaëtan Gilbert (Apr 18 2023 at 08:09):

I guess you could add merlin-lib to the coqc dependencies
or the vernac/dune dependencies if you want to be sure that coqtop coqidetop etc all get it

Stream: Coq devs & plugin devs

Topic: Dnylink Error when trying to add merlin-lib as dependency

Alperen Keles (Apr 17 2023 at 16:17):

Gaëtan Gilbert (Apr 17 2023 at 16:20):

Rodolphe Lepigre (Apr 18 2023 at 07:41):

Gaëtan Gilbert (Apr 18 2023 at 08:09):