Since I've updated my master branch, I can't get coq to compile anymore due to ld dying in the VM compilation
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
Any idea how to fix my installation?
(inb4 git clean -xdff)
(So it's not #11742, so now I have no idea why this is broken.)
did you change ocaml version recently?
Not that I know.
Coq was compiling yesterday night, I didn't do anything specific and now after a git fetch it's broken...
It's working with another opam switch, so something strange happened on my installation?
Hum, instead it looks like Coq is broken with OCaml 4.06.1
I have the same problem on another 4.06.1 switch
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)
Starting from 4.07 native compilation is prohibitively slow on some extreme examples though
That's one one the reasons I stick to 4.06
Anyways can somebody else confirm that Coq compilation is broken on 4.06.1?
I can do it, I need to test out some stuff on master
anyway (time to stare into the abyss again)
Thx
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.
@Pierre-Marie Pédrot installation of Coq master
on 4.06.1 worked fine for me on Ubuntu Linux
Weird, so something is wrong with my machine.
So there is indeed a change in the ocaml source code w.r.t. these redefined constants
Starting from 4.07 they are declared extern which is why the linker doesn't complain
Now the mystery is why coq compiled on my machine before
note that I only tried the default 4.06.1, not fp
or flambda
.
Maybe I updated ld without realizing and its default behaviour changed?
I tried only +fp and +flambda but I don't see why this would change anything
The files causing the error are similar in vanilla 4.06
looks like this: https://github.com/ocaml/ocaml/pull/1770
so the issues are with the specific linker used by the OCaml compiler?
or the C compiler, I don't know
ah, this in effect means one should consider GCC/Clang, ld, etc. as part of the Coq ecosystem
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
my versions of gcc and ld are older (think Ubuntu 18)
I update my computer regularly (I live on Debian unstable) so it's probably what caused the breakage
But this probably means that it'll happen to other users as well
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
Maybe there is a way to silence the linker though
The OCaml PR says that the error is actually a linker warning promoted by ocamlmklib
Indeed, by passing the right option to the GCC linker it goes through
Bug reported at https://github.com/coq/coq/issues/12940
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?
Not that I know of, it's buried inside the OCaml issue.
Would you mind opening one with pointers to the various OCaml issues?
At some point we could try to see if we manage to fix things on the OCaml side
The other useful information for Coq users/devs is what are the impacted OCaml versions
Last updated: Dec 07 2023 at 09:01 UTC