Undefined symbols when loading printers · Coq devs & plugin devs

I try to see how far I get with running an opam installed coqtop.byte under ocamldebug. Basically this works using ocamldebug-coq.run with a custom wrapper script to set the environment appropriate for opam. But I have issues loading the printers. I am doung "source db" and get :

(ocd) source db
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/ocaml/threads/threads.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/ocaml/str.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/zarith/zarith.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/coq/config/config.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/coq/clib/clib.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/ocaml/dynlink.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/coq/lib/lib.cma loaded
File /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/coq/gramlib/.pack/gramlib.cma loaded
Error during code loading: error while linking /Users/msoegtrop/.opam/_coq-platform_.2021.02.0/lib/coq/kernel/kernel.cma.
The external function `coq_uint63_to_float_byte' is not available

Reference to undefined global `Libnames'
Reference to undefined global `Names'

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:15):

Michael Soegtrop (Apr 01 2021 at 19:38):

Sorry, the documentation in debugging.md is a bit to terse for my OCaml skill level.
I am doing the following:

#!/bin/sh
export OCAMLDEBUG="$(which ocamldebug)"
export COQTOP="$(coqc -where)"
export CAML_LD_LIBRARY_PATH=$CAML_LD_LIBRARY_PATH:$(coqc -where)/kernel/byterun
source ./ocamldebug-coq.run "$(which coqtop.byte)"

to get around the fact that I don't have the generated ocamldebug-coq script in opam. Furthermore I have an .ocamlinit file with

#use "topfind";;

set arguments <my Q and R arguments>
set bigstep 10000000
set smallstep 1000000
run

This starts Coq. Then I drop to ocamltop with Drop.. How would I load the coqrun library? I guess it is the one in /lib/coq/kernel/byterun/libcoqrun.a? And I guess I should load it from my .ocamlinit file? But I can't figure out the correct library name or my path is wrong - neither with topfind syntax nor with plain OCaml syntax. The topfind list command shows me many coq related libraries, e.g.

coq.lib             (version: 8.13)

Michael Soegtrop (Apr 01 2021 at 19:39):

Michael Soegtrop (Apr 02 2021 at 06:24):

@Emilio Jesús Gallego Arias : can it be that the coq opam package simply does not install the coqrun library? I only have a file lib/coq/kernel/byterun/libcoqrun.a and I guess this is nothing ocaml or ocamldebug could load.

Guillaume Melquiond (Apr 02 2021 at 06:38):

You will never have more than that. libcoqrun.a is a pure C library. There is no OCaml involved. What one is supposed to do is to pass option -dllib -lcoqrun to force linking a C library (possibly with -dllpath if the library is hidden somewhere). But I have no idea if those options are supported by ocaml and ocamldebug.

Michael Soegtrop (Apr 02 2021 at 07:06):

Well at least on Windows without opam there was also a dllcoqrun.dll. On Mac with opam, the .a file is the only file with coqrun in the name. I will just build Coq and see if I can find it.

Guillaume Melquiond (Apr 02 2021 at 07:21):

On Linux, similarly to Windows, you have libcoqrun.so. So, perhaps, there is something botched for Mac's installation.

Michael Soegtrop (Apr 02 2021 at 07:56):

When I build Coq using the same method as opam does, I get a file named "dllcoqrun.so". I guess it should be named "libcoqrun.so" and that might be the reason why it doesn't get installed on Mac. I will see which name works and then file a bug.

Guillaume Melquiond (Apr 02 2021 at 08:02):

No, sorry, dllcoqrun.so is just fine. That is a historical artifact of the way OCaml shared libraries were built, but that is nonetheless the name expected by OCaml. (That said, that might still be the reason why it does not get installed.)

Guillaume Melquiond (Apr 02 2021 at 08:09):

If I understand correctly, dllcoqrun.so is not installed if the -custom flag was used, which is the default on Windows and Darwin, unless -no-custom was passed to configure.

Guillaume Melquiond (Apr 02 2021 at 08:11):

(Which makes sense I guess, since -custom means that coqrun was already statically linked to Coq binaries.)

Michael Soegtrop (Apr 02 2021 at 08:11):

Hmm, somehow I can't get this to work. I tried this in a fresg Coq 8.13.1 git folder:

git clean -d -f -X
./configure -local
make -j 16
make -j 16 byte
cd dev
./ocamldebug-coq coqtop.byte

Error during code loading: error while linking /Users/msoegtrop/CoqGit/coq-ref/kernel/kernel.cma.
The external function `coq_uint63_to_float_byte' is not available

Michael Soegtrop (Apr 02 2021 at 08:12):

Hmm, but I think ocamldebug also needs this shared library in order to be able to load the printers.

Michael Soegtrop (Apr 02 2021 at 08:13):

Guillaume Melquiond (Apr 02 2021 at 08:14):

Does that change something if you pass the flags -custom or -no-custom to configure?

Michael Soegtrop (Apr 02 2021 at 08:18):

Actually even without -no-custom coqtop.byte is not statically linked. It does not run if dllcoqrun is not in the path. Mysterious. This seems to be different from what opam does although I use the same options besides path spec options.

Michael Soegtrop (Apr 02 2021 at 08:32):

I am a bit lost here. The main information I am missing is how to tell ocamldebug to load a shared library needed by a printer. As far as I can tell this is not automatic and also kernel.cma doesn't seem to contain a reference to coqrun, but it does contain a reference to coq_uint63_to_float_byte which is defined in dllcoqrun.so.

Guillaume Melquiond (Apr 02 2021 at 08:45):

If you run ocamlobjinfo kernel.cma, it is supposed to tell you something like Extra dynamically-loaded libraries: -lcoqrun. That is how OCaml knows the dependencies.

Guillaume Melquiond (Apr 02 2021 at 08:50):

Basically, kernel.cma is built with the command line ocamlc -dllib -lcoqrun -a -o kernel.cma, which causes OCaml to indicate inside kernel.cma that dllcoqrun.so / libcoqrun.a is needed for execution / compilation.

Michael Soegtrop (Apr 02 2021 at 08:58):

Extra dynamically-loaded libraries:

So I guess the Mac build is some strange hybrid between statically and dynamically linked. As I said, coqtop.byte definitely does not run if it cannot find dllcoqrun.so.
I will experiment with -custom and -no-custom.

Michael Soegtrop (Apr 02 2021 at 09:26):

@Guillaume Melquiond : with ./configure -local -no-custom things do work. I get:

coq-ref$ ocamlobjinfo kernel/kernel.cma | head -n 10
:
Extra dynamically-loaded libraries: -lcoqrun

Guillaume Melquiond (Apr 02 2021 at 09:27):

Michael Soegtrop (Apr 02 2021 at 09:28):

Michael Soegtrop (Apr 02 2021 at 09:30):

Guillaume Melquiond (Apr 02 2021 at 09:34):

Yes, in -custom mode, C libraries such as libcoqrun.a are statically linked inside the binaries. So, it might have been used on Windows and Mac because the system was not able to find the libraries otherwise, so better stick them inside the executable files.

Michael Soegtrop (Apr 02 2021 at 09:38):

But since bytecode files are mostly used for debugging it doesn't make that much sense if the debugger doesn't work then.

Anyhow the -custom build seems to be a strange hybrid because the dllcoqrun.so is there and needed (also by coqtop.byte), but not referenced e.g. by kernel.cma.

I will also do a build with explicit -custom. Maybe this is yet something else ...

Guillaume Melquiond (Apr 02 2021 at 09:46):

That is strange, in -custom mode, libcoqrun.a should directly be linked into coqtop.byte and dllcoqrun.so would thus not be needed.

Guillaume Melquiond (Apr 02 2021 at 09:47):

I just tested it on Linux, ./configure -custom properly causes libcoqrun.a to be embedded.

Michael Soegtrop (Apr 02 2021 at 09:53):

@Guillaume Melquiond : sorry, my bad. I did a git clean -d -f -X instead of a git clean -d -f -x so something remained from the previous build.

In a proper clean -custom build, coqtop.byte does not depend on dllcoqrun.so.

But there is still the problem that dllcoqrun.so is actually there, kernel.cma needs it to get coq_uint63_to_float_byte but does not load it. So is this a link error in kernel.cma - should it statically link libcoqrun.a?

Michael Soegtrop (Apr 02 2021 at 09:54):

Guillaume Melquiond (Apr 02 2021 at 10:01):

The thing is, kernel.cma should not need it, as libcoqrun.a was embedded into coqtop.byte:

$ objdump -x bin/coqtop.byte | grep coq_uint63_to_float_byte
0000000000035a70 g     F .text  0000000000000016              coq_uint63_to_float_byte

Guillaume Melquiond (Apr 02 2021 at 10:03):

(ocd) source db
...
File gramlib.cma loaded
Error during code loading: error while linking kernel.cma.
The external function `coq_uint63_to_float_byte' is not available

Guillaume Melquiond (Apr 02 2021 at 10:08):

Hmm... According to the documentation of Ocamldebug, load_printer kernel.cma does not give access to the modules of the debugged program. That is why it does not find the content of libcoqrun.a.

Michael Soegtrop (Apr 02 2021 at 10:11):

Yes, ocamldebug needs its own copy of all functions used by the printers. With the -no-custom build this does work since kernel.cma references the shared library then.

Michael Soegtrop (Apr 02 2021 at 10:13):

Do you think this did ever work with -custom or is this a new issue introduced by new dependencies in kernel.cma (the name of the missing function looks new ...).

Emilio Jesús Gallego Arias (Apr 02 2021 at 11:04):

Actually I don't know how the make-based build works, for the dune one, we generate an empty cma which triggers the loading of the so file with its linking flags, so I dunno, after the pr switching the ocaml build for dune this should work.

Michael Soegtrop (Apr 02 2021 at 12:01):

@Emilio Jesús Gallego Arias : ok, then I will wait with further investigations. For the time being I can live with a -no-custombuild.

Stream: Coq devs & plugin devs

Topic: Undefined symbols when loading printers

Michael Soegtrop (Apr 01 2021 at 18:07):