[Coq plugin] Dynlink error on dependency of external library Atdgen #5998
Comments
|
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:
It adds:
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 I also thought of building with Coq 8.16, but I have had difficulties installing it on NixOS. But maybe I will try again. |
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: Champitoad/coq-plugin-template-atdgen#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 But 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 |
|
I'm not entirely sure how that should be fixed; I only have some pointers. coq/coq#16319 suggests that I do not understand how to fix this, but at least in part that's because I don't understand OCaml linking/findlib/ |
|
FWIW, the underlying problem might be #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 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.0and 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_foundwhich 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 $ 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 I cannot even build with a Makefile anymore. After adding the following 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_makefileworks, dune gives me the following error:It looks like Coq is unable to load the
Bi_iodependency ofAtdgen, even though it appears in the generatedmy_plugin.cmxs. I use theCohttplibrary 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
dunewith the--verboseflag): https://gist.github.com/Champitoad/dc380a29dafaac0df272af1a6b6a8498The text was updated successfully, but these errors were encountered: