Dynamic linking error via a Coq plugin or running an executable

[rlepigre]

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

[ejgallego]

@rlepigre your coq/dune file is:

(coq.theory
 (name bug)
 (stdlib no)
 (package bug))

So indeed, unless I'm missing something, how are thing supposed to work if you don't declare the dependency to your plugin?

[ejgallego]

Declaring the plugin we get a bit further:

$ (cd _build/default && /home/egallego/.opam/coq-v8.19/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -noinit -boot -I /home/egallego/.opam/coq-v8.19/lib/curl -I /home/egallego/.opam/coq-v8.19/lib/ocaml -I lib -R coq bug coq/bug.v)

File "./coq/bug.v", line 1, characters 0-31:
Error:
Findlib error: bug.plugin not found in:
/home/egallego/.opam/coq-v8.19/lib/curl
/home/egallego/.opam/coq-v8.19/lib/ocaml
lib
/home/egallego/.opam/coq-v8.19/lib

For some reason it seems that Coq is not reading OCAMLPATH ?

That seems bizarre to me.

[rlepigre]

So indeed, unless I'm missing something, how are thing supposed to work if you don't declare the dependency to your plugin?

Indeed, seems like I forgot this while minimizing.

[rlepigre]

For some reason it seems that Coq is not reading OCAMLPATH ?

That is always the case when you try running such commands shown by dune, you need to run with OCAMLPATH=_build/install/default/lib or something like that. At least that's what I do so that local plugins are found.

[ejgallego]

After a bit more hackery I'm back to the original error:

Dynlink error: no implementation available for Curl
Raised at Dynlink_common.Make.check_implementation_imports.(fun) in file "otherlibs/dynlink/dynlink_common.ml", line 173, characters 54-118
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dynlink_common.Make.check.(fun) in file "otherlibs/dynlink/dynlink_common.ml", line 235, characters 11-70
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Dynlink_common.Make.check in file "otherlibs/dynlink/dynlink_common.ml", line 233, characters 6-183
Called from Dynlink_common.Make.load in file "otherlibs/dynlink/dynlink_common.ml", line 333, characters 24-64
Re-raised at Dynlink_common.Make.load in file "otherlibs/dynlink/dynlink_common.ml", line 345, characters 8-17
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Fl_dynload.load_pkg in file "fl_dynload.ml", line 37, characters 5-227

[ejgallego]

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.