Pierre-Marie Pédrot (Aug 29 2020 at 10:33): 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
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
The only commit that might trigger this behaviour is I believe the merge of #11742, but I don't understand why
Pierre-Marie Pédrot (Aug 29 2020 at 10:35):Any idea how to fix my installation?
Pierre-Marie Pédrot (Aug 29 2020 at 10:35):(inb4 git clean -xdff)
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.)
Gaëtan Gilbert (Aug 29 2020 at 11:01):did you change ocaml version recently?
Pierre-Marie Pédrot (Aug 29 2020 at 11:50):Not that I know.
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...
Pierre-Marie Pédrot (Aug 29 2020 at 11:59):It's working with another opam switch, so something strange happened on my installation?
Pierre-Marie Pédrot (Aug 29 2020 at 12:08):Hum, instead it looks like Coq is broken with OCaml 4.06.1
Pierre-Marie Pédrot (Aug 29 2020 at 12:08):I have the same problem on another 4.06.1 switch
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)
Pierre-Marie Pédrot (Aug 29 2020 at 12:13):Starting from 4.07 native compilation is prohibitively slow on some extreme examples though
Pierre-Marie Pédrot (Aug 29 2020 at 12:13):That's one one the reasons I stick to 4.06
Pierre-Marie Pédrot (Aug 29 2020 at 12:13):Anyways can somebody else confirm that Coq compilation is broken on 4.06.1?
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)
Pierre-Marie Pédrot (Aug 29 2020 at 12:15):Thx
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.
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
Pierre-Marie Pédrot (Aug 29 2020 at 12:35):Weird, so something is wrong with my machine.
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
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
Pierre-Marie Pédrot (Aug 29 2020 at 12:47):Now the mystery is why coq compiled on my machine before
Karl Palmskog (Aug 29 2020 at 12:48):note that I only tried the default 4.06.1, not fp or flambda.
Pierre-Marie Pédrot (Aug 29 2020 at 12:48):Maybe I updated ld without realizing and its default behaviour changed?
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
Pierre-Marie Pédrot (Aug 29 2020 at 12:48):The files causing the error are similar in vanilla 4.06
Pierre-Marie Pédrot (Aug 29 2020 at 12:53):looks like this: https://github.com/ocaml/ocaml/pull/1770
Karl Palmskog (Aug 29 2020 at 12:54):so the issues are with the specific linker used by the OCaml compiler?
Pierre-Marie Pédrot (Aug 29 2020 at 12:54):or the C compiler, I don't know
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
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
pm@ouranos:~/sources/coq/kernel/byterun$ ld --version
GNU ld (GNU Binutils for Debian) 2.35
This particular linking problem has been solved in OCaml 4.07 though
Karl Palmskog (Aug 29 2020 at 12:57):my versions of gcc and ld are older (think Ubuntu 18)
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
Pierre-Marie Pédrot (Aug 29 2020 at 12:58):But this probably means that it'll happen to other users as well
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
Pierre-Marie Pédrot (Aug 29 2020 at 13:04):Maybe there is a way to silence the linker though
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
Pierre-Marie Pédrot (Aug 29 2020 at 13:08):Indeed, by passing the right option to the GCC linker it goes through
Pierre-Marie Pédrot (Aug 29 2020 at 13:23):Bug reported at https://github.com/coq/coq/issues/12940
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?
Pierre-Marie Pédrot (Aug 31 2020 at 14:27):Not that I know of, it's buried inside the OCaml issue.
Maxime Dénès (Aug 31 2020 at 14:28):Would you mind opening one with pointers to the various OCaml issues?
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
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: Dec 07 2023 at 09:01 UTC