I am trying to use Dynlink
to load the coq-core.stm
package at runtime:
let () =
Findlib.init ();
Dynlink.allow_unsafe_modules true;
Fl_dynload.load_packages ~debug:true ["coq-core.stm"]
The code above succeeds in bytecode but fails in native code.
[...]
[DEBUG] Fl_dynload: loading "coqrun.cmxs"
[...]
[DEBUG] Fl_dynload: loading "kernel.cmxs"
Fatal error: exception Dynlink.Error (Dynlink.Cannot_open_dll "Dynlink.Error (Dynlink.Cannot_open_dll \"Failure(\\\"/home/tmartine/.opam/4.13/lib/coq-core/kernel/kernel.cmxs: undefined symbol: coq_int_tcode\\\")\")")
If I understand correctly, the problem is that the symbol coq_int_tcode
is defined in the library coqrun
, which does not contain any OCaml code: since there is no external
definition referring to coq_int_tcode
, the C library is not linked to coqrun.cmxs
.
Here is a minimal example to reproduce this problem (one library c_lib
which defines a symbol c_lib_hello
, one library ocaml_lib
which uses this symbol, and one executable test_dynlink
which dynamically loads both: the execution succeeds in bytecode, but fails in native code):
mkdir test_dynlink
cd test_dynlink
cat >c_lib.c <<EOF
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <stdio.h>
value
c_lib_hello(void)
{
CAMLparam0();
printf("Hello, world!\n");
CAMLreturn(Val_unit);
}
EOF
cat >ocaml_lib.ml <<EOF
external c_lib_hello : unit -> unit = "c_lib_hello"
let () =
c_lib_hello ()
EOF
cat >test_dynlink.ml <<EOF
let () =
Dynlink.allow_unsafe_modules true;
Dynlink.loadfile (Dynlink.adapt_filename "c_lib.cma");
Dynlink.loadfile (Dynlink.adapt_filename "ocaml_lib.cma")
EOF
cat >dune <<EOF
(library
(name c_lib)
(modules)
(foreign_stubs
(language c)
(names c_lib)))
(library
(name ocaml_lib)
(modules ocaml_lib))
(executable
(name test_dynlink)
(modules test_dynlink)
(modes byte exe)
(libraries dynlink))
EOF
echo "(lang dune 2.0)" >dune-project
dune build
cd _build/default
LD_LIBRARY_PATH=. ./test_dynlink.bc
# Output: Hello, world!
./test_dynlink.exe
# undefined symbol: c_lib_hello
dune
is not the culprit; we can exhibit the same behavior by compiling by hand:
ocamlc -c c_lib.c
ocamlmklib -o c_lib c_lib.o
ocamlc -a -dllib -lc_lib -o c_lib.cma
ocamlc -a ocaml_lib.ml -o ocaml_lib.cma
ocamlc dynlink.cma test_dynlink.ml -o test_dynlink.bc
LD_LIBRARY_PATH=. ./test_dynlink.bc
# Output: Hello, world!
ocamlopt -shared -cclib "-L. -lc_lib" -o c_lib.cmxs
ocamlopt -shared ocaml_lib.ml -o ocaml_lib.cmxs
ocamlopt dynlink.cmxa test_dynlink.ml -o test_dynlink.exe
./test_dynlink.exe
# undefined symbol: c_lib_hello
One way to fix the problem is to force the linker to link with c_lib
by using --whole-archive
:
ocamlopt -shared -cclib "-Xlinker --whole-archive -L. -lc_lib -Xlinker --no-whole-archive" -o c_lib.cmxs
./test_dynlink.exe
# Output: Hello, world!
But I don’t know how to ask dune
to do that…