Stream: Coq devs & plugin devs

Topic: Undefined symbols when loading printers


view this post on Zulip Michael Soegtrop (Apr 01 2021 at 18:07):

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

A few other printers have:

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

Am I doing something wrong?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 18:15):

You need to load the coqrun library before kernel

view this post on Zulip 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:

I wrote a script:

#!/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";;

Then I start Coq with these ocamldebug commands:

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)

but nothing which looks like coqrun.

view this post on Zulip Michael Soegtrop (Apr 01 2021 at 19:39):

P.S.: I am on macOS

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

then at the ocd prompt:

source db

which results in:

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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 02 2021 at 08:13):

But in my local installation the file is there ...

view this post on Zulip Guillaume Melquiond (Apr 02 2021 at 08:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 02 2021 at 08:58):

Guillaume Melquiond said:

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.

I get this:

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.

view this post on Zulip 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

and the source db in ocamldebug does work. Thanks for the support!

So should the macOS build be changed to use -no-custom?

view this post on Zulip Guillaume Melquiond (Apr 02 2021 at 09:27):

No idea. I suppose there was some good reason to force -custom on macOS.

view this post on Zulip Michael Soegtrop (Apr 02 2021 at 09:28):

Possibly with an emphasis on was...

view this post on Zulip Michael Soegtrop (Apr 02 2021 at 09:30):

Does this only impacts byte code builds?

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Apr 02 2021 at 09:47):

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

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Apr 02 2021 at 09:54):

Btw.: does loading the debug printers in a -custom build work on linux?

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Apr 02 2021 at 10:03):

But indeed, it does not work on Linux either:

(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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ...).

view this post on Zulip 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.

view this post on Zulip 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.


Last updated: Oct 16 2021 at 02:03 UTC