-
Notifications
You must be signed in to change notification settings - Fork 394
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Dynamic linking error via a Coq plugin or running an executable #10659
Comments
@rlepigre your
So indeed, unless I'm missing something, how are thing supposed to work if you don't declare the dependency to your plugin? |
Declaring the plugin we get a bit further:
For some reason it seems that Coq is not reading That seems bizarre to me. |
Indeed, seems like I forgot this while minimizing. |
That is always the case when you try running such commands shown by dune, you need to run with |
After a bit more hackery I'm back to the original error:
|
There is something very strange going on here, will have look into this later on when i allocate the time to head towards dune-coq 1.0 language. |
File bug.tar.gz (updated) contains a small dune project that exhibits an issue related to dynamic linking. It is not clear to me whether the problem lies with dune itself, or with the involved packages, but there is some evidence showing that dune is somehow involved.
The archive contains a Coq plugin and a library loading it (CC @ejgallego @Alizter), as well as a standalone ocaml executable, both exhibiting unexpected behaviour as far as I can tell. Here is the contents of the archive:
The included
README.md
file explains how to reproduce the issues, assumingezcurl-lwt
is available. Note that some of the tests just rely oncurl
(part of theocurl
package, which is a dependency ofezcurl
).The text was updated successfully, but these errors were encountered: