Stream: Coq devs & plugin devs

Topic: Need help with ocamlfind


view this post on Zulip Michael Soegtrop (Jul 05 2020 at 08:28):

A question to the ocaml experts: how does it work that ocamlfind tells ocaml to link non ocaml / system libraries? Specifically how does it happen that when I add "-package lablgtk3" to ocamlfind it links the pango system library? My issue is that it doesn't when linking coqide (built with opam on Windows). Is there on option to ocamlfind to print the options it passes to ocamlc rather than calling ocamlc?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 09:04):

Can someone please test what these commands give on Linux (in a context where you could build coqide):
ocamlfind query -recursive -l-format lablgtk3-sourceview3
ocamlfind query -recursive -a-format lablgtk3-sourceview3

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 09:04):

l-format says -ccopt -L/home/gaetan/.opam/4.07.1/lib/lablgtk3
a-format says nothing

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 09:17):

Thanks, interesting. Did you have the recursive option? I get quite a bit more for l-format?
So it seems to be normal that ocamfind knows in which folders the libraries are supposed to be, but doesn't know what the libraries are.

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 09:19):

Oh I missed the -recursive in your question

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 09:20):

recursive l-format

-ccopt -L/home/gaetan/.opam/4.07.1/lib/ocaml
-ccopt -L/home/gaetan/.opam/4.07.1/lib/ocaml
-ccopt -L/home/gaetan/.opam/4.07.1/lib/cairo2
-ccopt -L/home/gaetan/.opam/4.07.1/lib/ocaml
-ccopt -L/home/gaetan/.opam/4.07.1/lib/lablgtk3
-ccopt -L/home/gaetan/.opam/4.07.1/lib/lablgtk3-sourceview3

a-format still nothing

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 09:45):

IIUC the "basic" way to find native libraries like pango is to use pkg-config, and ocamlfind wraps that*:

pkg-config --cflags pango
pkg-config --libs pang

*Google's first evidence for "ocamlfind pkg-config" is in in https://github.com/ocaml/ocamlbuild/issues/48.

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 09:57):

and in some cases, you must help pkg-config by setting/extending PKG_CONFIG_PATH

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 09:59):

That is the theory, but this is not what seems to happen (I tried hand built and opam on Windows, OSX and Linux from Gaetan above).
E.g. pkg-config --libs gtksourceview-3.0 gives

-LC:/bin/cygwin_coq_platform_mingw/usr/x86_64-w64-mingw32/sys-root/mingw/lib -lgtksourceview-3.0 -lgtk-3 -lgdk-3 -lgdi32 -limm32 -lshell32 -lole32 -Wl,-luuid -lwinmm -ldwmapi -lsetupapi -lcfgmgr32 -lz -lpangowin32-1.0 -lpangocairo-1.0 -lpango-1.0 -latk-1.0 -lcairo-gobject -lcairo -lgdk_pixbuf-2.0 -lgio-2.0 -lgobject-2.0 -lglib-2.0 -lintl

One should expect that lablgtk3-sourceview3 depends on gtksourceview-3.0 but the output of ocamlfind query -recursive -a-format lablgtk3-sourceview3 or the output of ocamlfind opt -only-show for the coqide link command contains no trace of the pkg-config output - again this is the same on WIndows, OSX and Linux.

So I would conclude that the mechanism is something else.

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 10:16):

pkg-config --libs gtksourceview-3.0 says -lgtksourceview-3.0 -lgtk-3 -lgdk-3 -lpangocairo-1.0 -lpango-1.0 -lharfbuzz -latk-1.0 -lcairo-gobject -lcairo -lgdk_pixbuf-2.0 -lgio-2.0 -lgobject-2.0 -lglib-2.0 for me

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:24):

Yes, and as you wrote before:

a-format says nothing

So to me it doesn't look like ocamlfind asks pkg-config.
Actually in the coqide link step command line (obtained with ocamlfind -show-only) there are no system (non OCaml) libraries at all:

ocamlopt.opt.exe -rectypes -w +a-4-9-27-41-42-44-45-48-58-67 -safe-string -strict-sequence -I coqpp -I config -I clib -I lib -I kernel -I kernel/byterun -I library -I engine -I pretyping -I interp -I proofs -I gramlib/.pack -I parsing -I printing -I tactics -I vernac -I stm -I toplevel -I ide -I ide/protocol -g -O3 -unbox-closures -o bin/coqide.exe -ccopt "-subsystem windows" -thread -I C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/cairo2 -I C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3 -I C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3-sourceview3 C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\unix.cmxa C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml/threads\threads.cmxa C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\bigarray.cmxa C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/cairo2\cairo.cmxa C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3\lablgtk3.cmxa C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3-sourceview3\lablgtk3_sourceview3.cmxa C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\str.cmxa ide/ide_win32_stubs.o ide/coq_icon.o config/config.cmxa clib/clib.cmxa lib/lib.cmxa ide/protocol/ideprotocol.cmxa ide/ide.cmxa ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml

So somehow ocamlc seems to be able to figure this out on his own. Likely the cmxa files have references to system libraries.

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 10:28):

dune says
(cd _build/default && /home/gaetan/.opam/4.07.1/bin/ocamlopt.opt -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -g -o ide/coqide/coqide_main.exe /home/gaetan/.opam/4.07.1/lib/ocaml/str.cmxa -I /home/gaetan/.opam/4.07.1/lib/ocaml /home/gaetan/.opam/4.07.1/lib/ocaml/unix.cmxa -I /home/gaetan/.opam/4.07.1/lib/ocaml /home/gaetan/.opam/4.07.1/lib/ocaml/threads/threads.cmxa -I /home/gaetan/.opam/4.07.1/lib/ocaml clib/clib.cmxa config/config.cmxa lib/lib.cmxa ide/coqide/protocol/protocol.cmxa ide/coqide/core.cmxa /home/gaetan/.opam/4.07.1/lib/ocaml/bigarray.cmxa -I /home/gaetan/.opam/4.07.1/lib/ocaml /home/gaetan/.opam/4.07.1/lib/cairo2/cairo.cmxa -I /home/gaetan/.opam/4.07.1/lib/cairo2 /home/gaetan/.opam/4.07.1/lib/lablgtk3/lablgtk3.cmxa -I /home/gaetan/.opam/4.07.1/lib/lablgtk3 /home/gaetan/.opam/4.07.1/lib/lablgtk3-sourceview3/lablgtk3_sourceview3.cmxa -I /home/gaetan/.opam/4.07.1/lib/lablgtk3-sourceview3 ide/coqide/coqide_gui.cmxa ide/coqide/.coqide_main.eobjs/native/dune__exe__Coqide_main.cmx)

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 10:29):

Hm, the lablgtk3 build script seems to _wrap_ pkg-config — might be time to page @Emilio Jesús Gallego Arias
https://github.com/garrigue/lablgtk/blob/lablgtk3/src/dune
https://github.com/garrigue/lablgtk/blob/lablgtk3/tools/dune_config.ml

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:33):

I wonder how /.opam/4.07.1/lib/lablgtk3/lablgtk3.cmxa -I /home/gaetan/.opam/4.07.1/lib/lablgtk3 is suppoed to work.
The ocamlc man page says on -I:

Add the given directory to the list of directories searched for ... and C libraries specified with -cclib -l xxx

But there are no -cclib -l options at all. So I guess lablgtk3.cmxa references them.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 10:35):

pkg-config is wrapped to build the C stubs

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:37):

@Emilio Jesús Gallego Arias : do you know how this works? Do the .cmxa files reference the system libraries?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:37):

I mean why does the command line @Gaëtan Gilbert posted work?

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:39):

lablgtk3.cmxa does need quite a few system libraries to link and they are nowhere specified on the command line.

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 10:41):

  The following command-line options are recognized by ocamlopt(1).

  -a     Build  a  library  (.cmxa/.a file) with the object files (.cmx/.o files) given on the
          command line, instead of linking them into an executable file. The name  of  the  li‐
          brary must be set with the -o option.

         If  -cclib or -ccopt options are passed on the command line, these options are stored
          in the resulting .cmxa library.  Then, linking with this library  automatically  adds
          back  the -cclib and -ccopt options as if they had been provided on the command line,
          unless the -noautolink option is given. Additionally, a substring $CAMLORIGIN  inside
          a   -ccopt  options  will be replaced by the full path to the .cma library, excluding
          the filename.

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:43):

@Gaëtan Gilbert : thanks! Do you know if there is a way to display the links in a cmxa file?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 10:44):

I know how it works but cannot have a look now, please ping me after the workshop, sorry :(

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 10:45):

Michael Soegtrop said:

lablgtk3.cmxa does need quite a few system libraries to link and they are nowhere specified on the command line.

Yes they are, as provided by pkg-config; so if they are not likely pkg-config is broken

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:46):

@Emilio Jesús Gallego Arias : that's fine - I can drop coqide for the time beeing and work on the rest of the platform.

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:50):

so if they are not likely pkg-config is broken

pkg.config is a bit tricky in a cygwin / mingw cross environment. I have two pkg-config, one for cygwin and one for mingw libraries (that is pkg-config --dump-personality is different). I suspect that when building lablgtk it picks up the wrong one. So it would be interesting to know how dune picks pkg.config. Maybe for a test I delete the wrong one and rebuild the libraries.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 10:51):

I think the main answer to your question is the one provided by Gatean, the link flags are stored

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2020 at 10:51):

Dune will use the pkg-config that is available on path, so indeed, the path needs to be setup properly; keep in mind that dune cross-compilation profiles can modify this but I guess you are not using that.

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 10:53):

but I guess you are not using that.

Not that I would know of. As I said, I will try what happens if I temporarily hide the wrong one.

view this post on Zulip Gaëtan Gilbert (Jul 05 2020 at 12:31):

BTW ocamlobjinfo ~/.opam/4.07.1/lib/lablgtk3/lablgtk3.cmxa says

Extra C object files: -llablgtk3_stubs -lgtk-3 -lgdk-3 -lpangocairo-1.0 -lpango-1.0 -lharfbuzz -latk-1.0 -lcairo-gobject -lcairo -lgdk_pixbuf-2.0 -lgio-2.0 -lgobject-2.0 -lglib-2.0

plus lots of uninteresting stuff

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 13:42):

Gaëtan Gilbert said:

BTW ocamlobjinfo ~/.opam/4.07.1/lib/lablgtk3/lablgtk3.cmxa says

Thanks, very useful to debut this!

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 15:41):

After some more research I still don't understand what the issue is. Library finding does not seem to be the issue. When I call ocamlc/ocamlfind with -verbose it outputs the final linker command, which is:

flexlink
-chain mingw64
-stack 33554432
-exe
-link
"-municode"
-o "bin/coqide.exe"
"-LC:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\flexdll"
"-Lcoqpp"
"-Lconfig"
"-Lclib"
"-Llib"
"-Lkernel"
"-Lkernel/byterun"
"-Llibrary"
"-Lengine"
"-Lpretyping"
"-Linterp"
"-Lproofs"
"-Lgramlib/.pack"
"-Lparsing"
"-Lprinting"
"-Ltactics"
"-Lvernac"
"-Lstm"
"-Ltoplevel"
"-Lide"
"-Lide/protocol"
"-LC:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/cairo2"
"-LC:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3"
"-LC:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3-sourceview3"
"-LC:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\threads"
"-LC:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml"
-subsystem windows
"C:\bin\cygwin_coq_platform_mingw\tmp\camlstartup74ba0f.o"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\std_exit.o"
"ide/coqide_main.o"
"ide/coqide_os_specific.o"
"ide/ide.a"
"ide/protocol/ideprotocol.a"
"lib/lib.a"
"clib/clib.a"
"config/config.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\str.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3-sourceview3\lablgtk3_sourceview3.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3\lablgtk3.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/cairo2\cairo.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\bigarray.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml/threads\threads.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\unix.a"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\stdlib.a"
"-lcamlstr"

"-llablgtk3_sourceview3_stubs"
"-LC:/bin/cygwin_coq_platform_mingw/usr/x86_64-w64-mingw32/sys-root/mingw/lib"
"-lgtksourceview-3.0"
"-lgtk-3"
"-lgdk-3"
"-lgdi32"
"-limm32"
"-lshell32"
"-lole32"
"-Wl,-luuid"
"-lwinmm"
"-ldwmapi"
"-lsetupapi"
"-lcfgmgr32"
"-lz"
"-lpangowin32-1.0"
"-lpangocairo-1.0"
"-lpango-1.0"
"-latk-1.0"
"-lcairo-gobject"
"-lcairo"
"-lgdk_pixbuf-2.0"
"-lgio-2.0"
"-lgobject-2.0"
"-lglib-2.0"
"-lintl"

"-llablgtk3_stubs" <<<<< symbols used here
"-lgtk-3"
"-lgdk-3"
"-lgdi32"
"-limm32"
"-lshell32"
"-lole32"
"-Wl,-luuid"
"-lwinmm"
"-ldwmapi"
"-lsetupapi"
"-lcfgmgr32"
"-lz"
"-lpangowin32-1.0"
"-lpangocairo-1.0" <<<<<<<<<< symbols defined here
"-lpango-1.0"
"-latk-1.0"
"-lcairo-gobject"
"-lcairo"
"-lgdk_pixbuf-2.0"
"-lgio-2.0"
"-lgobject-2.0"
"-lglib-2.0"
"-lintl"

"-lcairo_stubs"
"-lfreetype"
"-lfontconfig"
"-lfreetype"
"-lcairo"
"-lbigarray"
"-lthreadsnat"
"-lunix"
"-lws2_32"
"-ladvapi32"
"ide/ide_win32_stubs.o"
"ide/coq_icon.o"
"C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/ocaml\libasmrun.a"
-lws2_32
-lversion

I get errors like:

/usr/lib/gcc/x86_64-w64-mingw32/9.2.0/../../../../x86_64-w64-mingw32/bin/ld:
C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3\liblablgtk3_stubs.a(cairo_pango_stubs.o): in function `caml_pango_cairo_error_underline_path':
/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/build/lablgtk3.3.1.1/_build/default/src/cairo_pango_stubs.c:177: undefined reference to `pango_cairo_error_underline_path'

If I look into the pangocairo library specified by the names and search path in the linker command line I get:

nm C:/bin/cygwin_coq_platform_mingw/usr/x86_64-w64-mingw32/sys-root/mingw/lib/libpangocairo-1.0.dll.a
:
d000009.o:
0000000000000000 i .idata$4
0000000000000000 i .idata$5
0000000000000000 i .idata$6
0000000000000000 i .idata$7
0000000000000000 t .text
0000000000000000 I __imp_pango_cairo_error_underline_path
                 U _head_libpangocairo_1_0_0_dll
0000000000000000 T pango_cairo_error_underline_path
:

I checked that the .dll.a as extension for the library is not the issue.

If someone has an idea on what the root cause of this might be, please let me know. I give up.

I thought about if it could be a linking order problem, but I don't see how. There are two objects linked after the libs, but they don't contain stuff referencing a lot of other stuff.

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 16:43):

Two hopefully stupid questions: (1) does flexlink find the libpangocairo you checked out? (2) Are all the binaries involved for the same bit-width or otherwise compatible? I ask because I see both -chain mingw64 , mingw64c and x86_64-w64-mingw32. To make it easier I see mingw-w64 also includes 32-bit binaries :-|

view this post on Zulip Michael Soegtrop (Jul 05 2020 at 17:56):

@Paolo G. Giarrusso : (1) it is a bit hard to tell, but I would ecpect that it would give an error that it can't find a library in case it can't. I tried to give a random name but it is not that easy to pass through ocamlfind. I will try to rename the library and see what happen sthen. (2) This is all 64 bit stuff. I don't have a 32 bit tool chain installed. The naming is for sure confusing. The toolchains are named:

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 18:41):

re (1), I was hoping for some -verbose option to flexlink. I don't trust Unix tooling to be usable, and IIRC I've had ld screw up such things — especially if there's something else it could find instead...

view this post on Zulip Paolo Giarrusso (Jul 05 2020 at 18:44):

but I hope it's clear I'm far from knowing what's going on :-)

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 06:10):

Paolo G. Giarrusso said:

but I hope it's clear I'm far from knowing what's going on :-)

Me neither ;-) It is good to have someone to talk - it gives new ideas. I concluded that it is time for good old ProcMon.

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 06:57):

I looked at it with ProcMon. All involved tools (flexlink, mingw-gcc, ld) read the files in the wrong order, that is libpangocairo before liblablgtk3_stubs. Also libpangocairo is read only once, although it is specified twice on the command line. I will consult Alain Frisch about this.


Last updated: Oct 16 2021 at 09:07 UTC