dune icon indicating copy to clipboard operation
dune copied to clipboard

Dynamic linking error via a Coq plugin or running an executable

Open rlepigre opened this issue 3 weeks ago • 6 comments

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).

rlepigre avatar Jun 19 '24 11:06 rlepigre