[Coq plugin] Dynlink error on dependency of external library Atdgen

[Champitoad]

trafficstars

I am trying to build a Coq plugin which uses the Atdgen library to handle serialization over HTTP of some custom datatypes. While using coq_makefile works, dune gives me the following error:

> dune build                                                                                                                                                       
File "./theories/Test.v", line 1, characters 0-30:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/data/Users/pablo/coq-plugin-template-atdgen/_build/default/src/my_plugin.cmxs: undefined symbol: camlBi_io\")")

It looks like Coq is unable to load the Bi_io dependency of Atdgen, even though it appears in the generated my_plugin.cmxs. I use the Cohttp library for my HTTP client, and I have a similar issue.

Reproduction

I made a little MWE based on coq-plugin-template:

git clone [email protected]:Champitoad/coq-plugin-template-atdgen.git
cd coq-plugin-template-atdgen/
opam pin add -ny .
opam install --deps-only coq-my-plugin
eval (opam env)
dune build

Specifications

• Version of dune (output of dune --version): 3.3.1
• Version of coq (output of coqc -v): 8.15.2
• Version of ocaml (output of ocamlc --version): 4.14.0
• Operating system (distribution and version): NixOS 22.05

Additional information

• Link to gist with verbose output (run dune with the --verbose flag): https://gist.github.com/Champitoad/dc380a29dafaac0df272af1a6b6a8498

[Blaisorblade]

I'm not a dune dev, just a Coq user, but https://github.com/Champitoad/coq-plugin-template-atdgen#linking-with-external-libraries explains this is expected:

If your plugin depends on an external OCaml library, Coq will fail to load it as it doesn't know about this dependency. [...] Meanwhile, you need to manage the dependency chain manually [... workaround explanation ...]

It adds:

This should be fixed in Coq hopefully soon, see https://github.com/coq/coq/issues/7698.

Indeed, there's been progress in Coq 8.16 (see link); the release which is in testing and should be released soon.

Does this help? If so, can you please close the issue?

[Champitoad]

Problem is, the workaround is just to add explicitly the external library (here atdgen or cohttp-lwt-unix) as a dependency in dune, which I already do with no success.

I also thought of building with Coq 8.16, but I have had difficulties installing it on NixOS. But maybe I will try again.

[Blaisorblade]

the workaround is just to add explicitly the external library (here atdgen or cohttp-lwt-unix) as a dependency in dune, which I already do with no success.

In the code you linked, you add the library as a dependency of your plugin. That's no workaround.

AFAICT, the docs recommend other changes as well: https://github.com/Champitoad/coq-plugin-template-atdgen/pull/1 is how I read them.

[Champitoad]

Indeed my mistake, I wasn't reading completely... So I implemented your suggestion, but it seemed like I had to dynamically load not only atdgen, but the transitive closure of all of its dependencies. And it still does not work, now I get the following error when loading atdgen_runtime:

Error: Dynlink error: no implementation available for Stream

But Stream should be in OCaml's standard library... Here is the commit: https://github.com/Champitoad/coq-plugin-template-atdgen/commit/cfae192c29a93d0efc45cf0c60834c7b2ef6df28

Even if it works in the end, it does seem more tractable to switch to Coq 8.16, so I will give that a shot.

[Champitoad]

Ok so I have successfully installed Coq 8.16, but I still get the same error, albeit now it looks like it uses findlib (commit link: https://github.com/Champitoad/coq-plugin-template-atdgen/commit/67913eb48b460dcc4b4b21cc36ab1816cade2914):

> dune build                                                                                                                                
File "./theories/MyPlugin.v", line 1, characters 0-51:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/data/Users/pablo/coq-plugin-template-atdgen/_build/default/src/my_plugin.cmxs: undefined symbol: camlBi_io\")")
Findlib paths:
/data/Users/pablo/coq-plugin-template-atdgen/_build/install/default/lib
/nix/store/a2mlfvsf4m01kn9w69knhwg9ympk8pxv-dune-2.9.3/lib/ocaml/4.14.0/site-lib/
/nix/store/6165ak4db99jaknab8jjqjqmwlsr5d5g-ocaml-findlib-1.9.3/lib/ocaml/4.14.0/site-lib/
/nix/store/9jgak210d8i74543av27xnsbgxcjni79-ocaml4.14.0-merlin-4.5-414/lib/ocaml/4.14.0/site-lib/
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/
/nix/store/5rq8ls4vvcbj5y9v0a74xvj4hckk7rri-ocaml4.14.0-zarith-1.12/lib/ocaml/4.14.0/site-lib/
/nix/store/6qwn3llwi8ykf1f7fmcwm0qckyy2b95w-ocaml4.14.0-atdgen-2.4.1/lib/ocaml/4.14.0/site-lib/
/nix/store/hlprnqspvj6c82fv314hnipwz5n856ai-ocaml4.14.0-atdgen-runtime-2.4.1/lib/ocaml/4.14.0/site-lib/
/nix/store/wvzr1id5dplc65jrdv4i95ny0ckk05rm-ocaml4.14.0-biniou-1.2.1/lib/ocaml/4.14.0/site-lib/
/nix/store/xrwr90bmswy74a2ybjzkpayrjwgnknyi-ocaml4.14.0-easy-format-1.3.3/lib/ocaml/4.14.0/site-lib/
/nix/store/jz7y3m20cpwr805n3sdhy2xwp1411355-ocaml4.14.0-camlp-streams-5.0/lib/ocaml/4.14.0/site-lib/
/nix/store/k5imygsr5y1h0vflkrg8b5mzv6bqd69n-ocaml4.14.0-yojson-1.7.0/lib/ocaml/4.14.0/site-lib/
/nix/store/a2mlfvsf4m01kn9w69knhwg9ympk8pxv-dune-2.9.3/lib/ocaml/4.14.0/site-lib/
/nix/store/6165ak4db99jaknab8jjqjqmwlsr5d5g-ocaml-findlib-1.9.3/lib/ocaml/4.14.0/site-lib/
/nix/store/9jgak210d8i74543av27xnsbgxcjni79-ocaml4.14.0-merlin-4.5-414/lib/ocaml/4.14.0/site-lib/
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/
/nix/store/5rq8ls4vvcbj5y9v0a74xvj4hckk7rri-ocaml4.14.0-zarith-1.12/lib/ocaml/4.14.0/site-lib/
/nix/store/6qwn3llwi8ykf1f7fmcwm0qckyy2b95w-ocaml4.14.0-atdgen-2.4.1/lib/ocaml/4.14.0/site-lib/
/nix/store/hlprnqspvj6c82fv314hnipwz5n856ai-ocaml4.14.0-atdgen-runtime-2.4.1/lib/ocaml/4.14.0/site-lib/
/nix/store/wvzr1id5dplc65jrdv4i95ny0ckk05rm-ocaml4.14.0-biniou-1.2.1/lib/ocaml/4.14.0/site-lib/
/nix/store/xrwr90bmswy74a2ybjzkpayrjwgnknyi-ocaml4.14.0-easy-format-1.3.3/lib/ocaml/4.14.0/site-lib/
/nix/store/jz7y3m20cpwr805n3sdhy2xwp1411355-ocaml4.14.0-camlp-streams-5.0/lib/ocaml/4.14.0/site-lib/
/nix/store/k5imygsr5y1h0vflkrg8b5mzv6bqd69n-ocaml4.14.0-yojson-1.7.0/lib/ocaml/4.14.0/site-lib/
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/btauto
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/cc
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/derive
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/extraction
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/firstorder
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/funind
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/ltac
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/ltac2
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/micromega
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/nsatz
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/number_string_notation
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/ring
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/rtauto
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/ssreflect
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/ssrmatching
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/tauto
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/tutorial
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/tutorial/p0
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/tutorial/p1
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/tutorial/p2
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/tutorial/p3
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/plugins/zify
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/../coq-core/..
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/coq/user-contrib/Ltac2
/nix/store/5rq8ls4vvcbj5y9v0a74xvj4hckk7rri-ocaml4.14.0-zarith-1.12/lib/ocaml/4.14.0/site-lib/zarith
/nix/store/6165ak4db99jaknab8jjqjqmwlsr5d5g-ocaml-findlib-1.9.3/lib/ocaml/4.14.0/site-lib/findlib
/nix/store/6qwn3llwi8ykf1f7fmcwm0qckyy2b95w-ocaml4.14.0-atdgen-2.4.1/lib/ocaml/4.14.0/site-lib/atdgen
/nix/store/9p8zf0as2dq9x1ay4nf0h58zaf1i2icz-ocaml-4.14.0/lib/ocaml
/nix/store/9p8zf0as2dq9x1ay4nf0h58zaf1i2icz-ocaml-4.14.0/lib/ocaml/threads
/nix/store/hlprnqspvj6c82fv314hnipwz5n856ai-ocaml4.14.0-atdgen-runtime-2.4.1/lib/ocaml/4.14.0/site-lib/atdgen-runtime
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/boot
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/clib
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/config
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/engine
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/gramlib
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/interp
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/kernel
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/lib
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/library
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/parsing
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/plugins/ltac
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/pretyping
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/printing
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/proofs
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/stm
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/sysinit
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/tactics
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/vernac
/nix/store/irfcpvxkzshz2jivxynlmzpn1751b8wi-coq-8.16+rc1/lib/ocaml/4.14.0/site-lib/coq-core/vm
/nix/store/jz7y3m20cpwr805n3sdhy2xwp1411355-ocaml4.14.0-camlp-streams-5.0/lib/ocaml/4.14.0/site-lib/camlp-streams
/nix/store/k5imygsr5y1h0vflkrg8b5mzv6bqd69n-ocaml4.14.0-yojson-1.7.0/lib/ocaml/4.14.0/site-lib/yojson
/nix/store/wvzr1id5dplc65jrdv4i95ny0ckk05rm-ocaml4.14.0-biniou-1.2.1/lib/ocaml/4.14.0/site-lib/biniou
/nix/store/xrwr90bmswy74a2ybjzkpayrjwgnknyi-ocaml4.14.0-easy-format-1.3.3/lib/ocaml/4.14.0/site-lib/easy-format
src
/nix/store/6165ak4db99jaknab8jjqjqmwlsr5d5g-ocaml-findlib-1.9.3/lib/ocaml/4.14.0/site-lib

[Blaisorblade]

I'm not entirely sure how that should be fixed; I only have some pointers.

https://github.com/coq/coq/pull/16319 suggests that dune does not generate yet the correct library metadata. See also https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Declare-ML-Module.

I do not understand how to fix this, but at least in part that's because I don't understand OCaml linking/findlib/META files.

[Blaisorblade]

FWIW, the underlying problem might be https://github.com/ocaml/dune/issues/5767, but that's an internal discussion in any case.

[ejgallego]

I know how this should be fixed, and I wrote it somewhere, but I don't know where.

[Alizter]

@ejgallego Any update with this?

[ejgallego]

Not really, either:

• you use the legacy loading method and load the deps by hand
• we fix https://github.com/coq/coq/issues/16571 and then the new legacy method should work for composed dune plugins.

[dwarfmaster]

I have the same error, and when trying to use the legacy method, it complains that it finds the Flags module twice, once in coq-core/lib and once in ocaml core_kernel/flags, and then fails with Dynlink error: The module Flags is already loaded.

Maybe I should open a separate issue ?

[Champitoad]

I have updated Coq and OCaml:

$ coqc -v
The Coq Proof Assistant, version 8.17.0
compiled with OCaml 5.0.0

and I've tried using the new loading syntax for Coq plugins, according to Dune's documentation. If I use the one for Coq 8.17:

Declare ML Module "coq-actema.plugin".

I get the following error:

$ dune build
File "./theories/Loader.v", line 1, characters 0-38:
Error:
Dynlink error: execution of module initializers in the shared library failed: Not_found

which is mentioned in the Coq manual, but not documented. So I tried the legacy-supporting syntax (supposedly for Coq 8.16 according to Dune's doc):

Declare ML Module "actema_plugin:coq-actema.plugin".

and then I go back to a Dynlink.Cannot_open_dll error:

$ dune build   
File "./theories/Loader.v", line 1, characters 0-52:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/mnt/data/plugin/_build/default/src/actema_plugin.cmxs: undefined symbol: camlUri\")")

Notice that this time the undefined symbol is camlUri, and I have no idea to which of my dependencies it is related (I've tried googling it with no success, or even adding the ocaml-uri lib as a dependency).

I cannot even build with a Makefile anymore. After adding the following META.coq-actema file in src:

package "actema" (
    directory = "."
    version = "dev"
    description = "Integrating the Actema GUI as a tactic."
    requires = "coq-core.plugins.ltac atdgen cohttp-lwt-unix sha"
    archive(byte) = "actema_plugin.cma"
    archive(native) = "actema_plugin.cmxa"
    plugin(byte) = "actema_plugin.cma"
    plugin(native) = "actema_plugin.cmxs"
)
directory = "."

I get exactly the same Dynlink.Cannot_open_dll error as with dune.

Thus for now I am stuck with using Coq 8.15 and OCaml 4.14. Do you have any idea of what's happening @ejgallego?