dune
dune copied to clipboard
Dynamic linking error via a Coq plugin or running an executable
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:
├── bug.opam
├── coq Coq theory
│ ├── bug.v File loading the plugin from the lib folder
│ └── dune
├── dune-project
├── junk
│ ├── dune
│ ├── main.ml Program using "findlib.dynload" to load "curl", "curl.lwt" and then "ezcurl-lwt"
│ └── Makefile Alternative way to compile "main.ml", using `ocamlfind ocamlopt`
├── lib
│ ├── dune
│ ├── lib.ml Coq plugin using a symbol from "curl"
│ └── plugin.mlpack
└── README.md
The included README.md
file explains how to reproduce the issues, assuming ezcurl-lwt
is available. Note that some of the tests just rely on curl
(part of the ocurl
package, which is a dependency of ezcurl
).