Stream: Coq devs & plugin devs

Topic: ld errors on master


view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 10:33):

Since I've updated my master branch, I can't get coq to compile anymore due to ld dying in the VM compilation

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 10:33):

Here is the excerpt:

cd kernel/byterun/ && \
"/home/pm/.opam/4.06.1+fp/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o
/usr/bin/ld : coq_interp.o:/home/pm/.opam/4.06.1+fp/lib/ocaml/caml/major_gc.h:69 : définitions multiples de « caml_major_work_credit »; coq_memory.o:/home/pm/.opam/4.06.1+fp/lib/ocaml/caml/major_gc.h:69 : défini pour la première fois ici
/usr/bin/ld : coq_interp.o:/home/pm/.opam/4.06.1+fp/lib/ocaml/caml/major_gc.h:68 : définitions multiples de « caml_major_ring_index »; coq_memory.o:/home/pm/.opam/4.06.1+fp/lib/ocaml/caml/major_gc.h:68 : défini pour la première fois ici
/usr/bin/ld : coq_interp.o:/home/pm/.opam/4.06.1+fp/lib/ocaml/caml/major_gc.h:67 : définitions multiples de « caml_major_ring »; coq_memory.o:/home/pm/.opam/4.06.1+fp/lib/ocaml/caml/major_gc.h:67 : défini pour la première fois ici
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile.build:355 : kernel/byterun/libcoqrun.a] Erreur 2

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 10:35):

The only commit that might trigger this behaviour is I believe the merge of #11742, but I don't understand why

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 10:35):

Any idea how to fix my installation?

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 10:35):

(inb4 git clean -xdff)

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 10:41):

(So it's not #11742, so now I have no idea why this is broken.)

view this post on Zulip Gaëtan Gilbert (Aug 29 2020 at 11:01):

did you change ocaml version recently?

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 11:50):

Not that I know.

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 11:53):

Coq was compiling yesterday night, I didn't do anything specific and now after a git fetch it's broken...

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 11:59):

It's working with another opam switch, so something strange happened on my installation?

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:08):

Hum, instead it looks like Coq is broken with OCaml 4.06.1

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:08):

I have the same problem on another 4.06.1 switch

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:09):

can this mean that we are finally going to go >= 4.07.1 only? :tada: if so (from my myopic perspective of dealing with 4.05.0 bugs in the Coq ecosystem 3 years after its release)

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:13):

Starting from 4.07 native compilation is prohibitively slow on some extreme examples though

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:13):

That's one one the reasons I stick to 4.06

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:13):

Anyways can somebody else confirm that Coq compilation is broken on 4.06.1?

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:14):

I can do it, I need to test out some stuff on master anyway (time to stare into the abyss again)

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:15):

Thx

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:17):

I wonder what a tag cloud with "Coq ecosystem issues 2020" would look like. My guess would be that there is a big fat "native compilation" in the middle.

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:32):

@Pierre-Marie Pédrot installation of Coq master on 4.06.1 worked fine for me on Ubuntu Linux

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:35):

Weird, so something is wrong with my machine.

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:46):

So there is indeed a change in the ocaml source code w.r.t. these redefined constants

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:46):

Starting from 4.07 they are declared extern which is why the linker doesn't complain

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:47):

Now the mystery is why coq compiled on my machine before

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:48):

note that I only tried the default 4.06.1, not fp or flambda.

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:48):

Maybe I updated ld without realizing and its default behaviour changed?

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:48):

I tried only +fp and +flambda but I don't see why this would change anything

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:48):

The files causing the error are similar in vanilla 4.06

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:53):

looks like this: https://github.com/ocaml/ocaml/pull/1770

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:54):

so the issues are with the specific linker used by the OCaml compiler?

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:54):

or the C compiler, I don't know

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:55):

ah, this in effect means one should consider GCC/Clang, ld, etc. as part of the Coq ecosystem

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:55):

FTR:

pm@ouranos:~/sources/coq/kernel/byterun$ gcc --version
gcc (Debian 10.2.0-5) 10.2.0

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:56):

pm@ouranos:~/sources/coq/kernel/byterun$ ld --version
GNU ld (GNU Binutils for Debian) 2.35

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:56):

This particular linking problem has been solved in OCaml 4.07 though

view this post on Zulip Karl Palmskog (Aug 29 2020 at 12:57):

my versions of gcc and ld are older (think Ubuntu 18)

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:57):

I update my computer regularly (I live on Debian unstable) so it's probably what caused the breakage

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 12:58):

But this probably means that it'll happen to other users as well

view this post on Zulip Karl Palmskog (Aug 29 2020 at 13:02):

opam doesn't even expose the compiler or linker version, so this is very hard to deal with in general (for end users) without going full >= 4.07

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 13:04):

Maybe there is a way to silence the linker though

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 13:04):

The OCaml PR says that the error is actually a linker warning promoted by ocamlmklib

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 13:08):

Indeed, by passing the right option to the GCC linker it goes through

view this post on Zulip Pierre-Marie Pédrot (Aug 29 2020 at 13:23):

Bug reported at https://github.com/coq/coq/issues/12940

view this post on Zulip Maxime Dénès (Aug 31 2020 at 14:25):

Pierre-Marie Pédrot said:

Starting from 4.07 native compilation is prohibitively slow on some extreme examples though

Is there an open issue about this?

view this post on Zulip Pierre-Marie Pédrot (Aug 31 2020 at 14:27):

Not that I know of, it's buried inside the OCaml issue.

view this post on Zulip Maxime Dénès (Aug 31 2020 at 14:28):

Would you mind opening one with pointers to the various OCaml issues?

view this post on Zulip Maxime Dénès (Aug 31 2020 at 14:28):

At some point we could try to see if we manage to fix things on the OCaml side

view this post on Zulip Maxime Dénès (Aug 31 2020 at 14:29):

The other useful information for Coq users/devs is what are the impacted OCaml versions


Last updated: Oct 15 2021 at 19:03 UTC