Open Champitoad opened 2 years ago
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?
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.
the workaround is just to add explicitly the external library (here
atdgen
orcohttp-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.
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.
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
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.
FWIW, the underlying problem might be https://github.com/ocaml/dune/issues/5767, but that's an internal discussion in any case.
I know how this should be fixed, and I wrote it somewhere, but I don't know where.
@ejgallego Any update with this?
Not really, either:
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 ?
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?
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:It looks like Coq is unable to load the
Bi_io
dependency ofAtdgen
, even though it appears in the generatedmy_plugin.cmxs
. I use theCohttp
library for my HTTP client, and I have a similar issue.Reproduction
I made a little MWE based on coq-plugin-template:
Specifications
dune
(output ofdune --version
): 3.3.1coq
(output ofcoqc -v
): 8.15.2ocaml
(output ofocamlc --version
): 4.14.0Additional information
dune
with the--verbose
flag): https://gist.github.com/Champitoad/dc380a29dafaac0df272af1a6b6a8498