Stream: Coq users

Topic: Can't install Coq 8.18.0 due to an undefined reference error


view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 06:02):

Hi. I'm trying to build Coq 8.18.0 via opam, but can't because of the following errors:

%LANG=C opam install coq
The following actions will be performed:
  - install coq-core      8.18.0 [required by coq]
  - install coqide-server 8.18.0 [required by coq]
  - install coq-stdlib    8.18.0 [required by coq]
  - install coq           8.18.0
===== 4 to install =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coq.8.18.0  (cached)
-> retrieved coq-core.8.18.0  (cached)
-> retrieved coq-stdlib.8.18.0  (cached)
-> retrieved coqide-server.8.18.0  (cached)
[ERROR] The compilation of coq-core.8.18.0 failed at "dune build -p coq-core -j 15 @install".

#=== ERROR while compiling coq-core.8.18.0 ====================================#
# context     2.1.3 | linux/x86_64 | ocaml.4.14.1 | https://opam.ocaml.org#b61304c6
# path        ~/.opam/default/.opam-switch/build/coq-core.8.18.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-core -j 15 @install
# exit-code   1
# env-file    ~/.opam/log/coq-core-15427-8bafff.env
# output-file ~/.opam/log/coq-core-15427-8bafff.out
### output ###
# [...]
# /home/hiroki/.opam/default/.opam-switch/build/zarith.1.13/z.ml:362: undefined reference to `ml_z_extract_small'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: /home/hiroki/.opam/default/lib/zarith/zarith.a(z.o): in function `camlZ__1':
# :(.data+0xc08): undefined reference to `ml_z_extract_small'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0xcf0): undefined reference to `ml_z_fits_nativeint_unsigned'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0xcf8): undefined reference to `ml_z_fits_int64_unsigned'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0xd00): undefined reference to `ml_z_fits_int32_unsigned'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0xd98): undefined reference to `ml_z_to_nativeint_unsigned'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0xda0): undefined reference to `ml_z_to_int64_unsigned'
# /usr/lib/gcc/x86_64-pc-linux-gnu/12/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0xda8): undefined reference to `ml_z_to_int32_unsigned'
# collect2: error: ld returned 1 exit status
# File "caml_startup", line 1:
# Error: Error during linking (exit code 1)



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-core 8.18.0
+-
- No changes have been performed

I tried to reinstall Zarith by opam reinstall zarith, but nothing changed.
Installing via opam is necessary because my OCaml project depends on it, and I did it successfully before.
What should I do? Thank you.

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 10:42):

Those functions should be provided by zarith and are written in C (https://github.com/ocaml/Zarith/blob/master/caml_z.c ). I wonder if the trouble is in the zarith build or in the Coq link command...

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 11:26):

Retried with --verbose. Log.
Seems like the cause is the mixed environment between my system-wide OCaml (installed by the system package manager Portage) and my local one installed by opam.

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 11:37):

What's the opam switch output?

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 11:39):

You did run eval $(opam env), right? But then the local ocaml should be on the PATH first, so it's surprising that in the verbose log, coq decided to install in /usr/bin:

-   OCaml binaries in           : /usr/bin/
-   OCaml library in            : /usr/lib64/ocaml

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 11:41):

Re "compiler choice", opam should either reuse the system compiler (by installing ocaml-system) _or_ build its own — in the latter case, then eval $(opam env) will put the the opam-built compiler on the PATH first.

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 12:44):

%opam switch
#  switch   compiler      description
  default  ocaml.4.14.1  default

Now I ran eval $(opam env) before the install command, but the error didn't go away. I appended the log to the gist.

My PATH:

/home/hiroki/.opam/default/bin:/home/hiroki/.cabal/bin:/home/hiroki/cquery/build/release/bin:/home/hiroki/.local/bin:/home/hiroki/.gem/ruby/2.6.0/bin:/home/hiroki/.gem/ruby/2.4.0/bin:/home/hiroki/.cargo/bin:/home/hiroki/go/bin:/home/hiroki/.ghcup/bin:/home/hiroki/.fly/bin:/home/hiroki/.zplug/bin:/home/hiroki/.cargo/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/opt/bin:/usr/lib/llvm/16/bin:/etc/eselect/wine/bin:/home/hiroki/git_repository/fzf/bin

I noticed that my opam is installed system-widely.

%where opam
/usr/bin/opam

ocaml is installed both for my user and system-widely.

%where ocaml
/home/hiroki/.opam/default/bin/ocaml
/usr/bin/ocaml

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 12:53):

hm, if you hadn't run eval $(opam env) earlier, maybe some install process used the wrong compiler?
a system-wide opam is normal, the system compiler is error-prone but eval $(opam env) _should_ shadow it properly.

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 12:59):

Sorry to confuse you, but it seems my .zshrc did initializations because my .zshrc had this line.

# opam configuration
[[ ! -r /home/hiroki/.opam/opam-init/init.zsh ]] || source /home/hiroki/.opam/opam-init/init.zsh  > /dev/null 2> /dev/null

And my PATH immediately after launching a new terminal (below) contained the path to ~/.opam/default/bin, so I don't think some packages are installed with the wrong compiler.

/home/hiroki/.opam/default/bin:/home/hiroki/.cabal/bin:/home/hiroki/cquery/build/release/bin:/home/hiroki/.local/bin:/home/hiroki/.gem/ruby/2.6.0/bin:/home/hiroki/.gem/ruby/2.4.0/bin:/home/hiroki/.cargo/bin:/home/hiroki/go/bin:/home/hiroki/.ghcup/bin:/home/hiroki/.fly/bin:/home/hiroki/.zplug/bin:/home/hiroki/.cargo/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/opt/bin:/usr/lib/llvm/16/bin:/etc/eselect/wine/bin:/home/hiroki/git_repository/fzf/bin

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 13:03):

Here is the log of opam reinstall zarith --verbose

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 13:25):

Okay that's good, the opam-init line _can_ imply an automatic eval $(opam env) (that's configurable IIRC), but the PATH from a new terminal looks good...

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 13:26):

I'm now wondering if zarith does have those symbols, or not: your verbose log doesn't seem to compile caml_c or invoke any C compiler! Sorry I'm blind, caml_z is built just fine

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 13:29):

it's probably just a bug in logging, so I'm seeing what I get locally

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 13:33):

The output of nm .opam/default/lib/zarith/zarith.a just in case.

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 13:47):

oh good so you know some of the troubleshooting here... U ml_z_extract_smallagrees that symbol is undefined — here it lives in libzarith.a not zarith.a.

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 13:54):

Ah, yes. It exists in libzarith.a.

%nm .opam/default/lib/zarith/libzarith.a|grep ml_z_extract_small
00000000000036f0 T ml_z_extract_small

Full log

view this post on Zulip Hiroki Tokunaga (Sep 17 2023 at 13:59):

Here is the log of opam reinstall coq-core --verbose on my laptop, which succeeded.

%opam reinstall coq-core --verbose
The following actions will be performed:
   recompile coq-core      8.17.1
   recompile coqide-server 8.17.1        [uses coq-core]
   recompile coq-stdlib    8.17.1        [uses coq-core]
   recompile coq           8.17.1        [uses coq-core]
   recompile coq-serapi    8.17.0+0.17.0 [uses coq]
   recompile coqfmt        0.1.0*        [uses coq]
=====  6 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
 retrieved coq-serapi.8.17.0+0.17.0  (cached)
 retrieved coq-core.8.17.1  (cached)
 retrieved coq.8.17.1  (cached)
 retrieved coq-stdlib.8.17.1  (cached)
 retrieved coqide-server.8.17.1  (cached)
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "-prefix" "/home/hiroki/.opam/default" "-mandir" "/home/hiroki/.opam/default/man" "-libdir" "/home/hiroki/.opam/default/lib/coq" "-native-compiler" "no" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coq-core.8.17.1)
- You have OCaml 4.14.1. Good!
- You have OCamlfind 1.9.6. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.13 installed. Good!
-
-   Architecture                : Linux
-   Sys.os_type                 : Unix
-   OCaml version               : 4.14.1
-   OCaml binaries in           : /usr/bin/
-   OCaml library in            : /usr/lib64/ocaml
-   Web browser                 : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
-   Coq web site                : http://coq.inria.fr/
-   Bytecode VM enabled         : true
-   Native Compiler enabled     : no
-
-   Paths where installation is expected by Coq Makefile:
-   - Coq is expected in /home/hiroki/.opam/default
-   - the Coq library is expected in /home/hiroki/.opam/default/lib/coq
-   - the Coqide configuration files is expected in /home/hiroki/.opam/default/etc/xdg/coq
-   - the Coqide data files is expected in /home/hiroki/.opam/default/share/coq
-   - the Coq man pages is expected in /home/hiroki/.opam/default/man
-   - documentation prefix path for all Coq packages is expected in /home/hiroki/.opam/default/share/doc
-
- If anything is wrong above, please restart './configure'.
-
- *Warning* To compile the system for a new architecture
-           don't forget to do a 'make clean' before './configure'.
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "dune" "build" "-p" "coq-core" "-j" "7" "@install" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coq-core.8.17.1)
λ compiled  coq-core.8.17.1
 removed   coqfmt.0.1.0
 removed   coq-serapi.8.17.0+0.17.0
 removed   coq.8.17.1
 removed   coq-stdlib.8.17.1
 removed   coqide-server.8.17.1
 removed   coq-core.8.17.1
 installed coq-core.8.17.1
- You have OCaml 4.14.1. Good!
- You have OCamlfind 1.9.6. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.13 installed. Good!
-
-   Architecture                : Linux
-   Sys.os_type                 : Unix
-   OCaml version               : 4.14.1
-   OCaml binaries in           : /usr/bin/
-   OCaml library in            : /usr/lib64/ocaml
-   Web browser                 : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
-   Coq web site                : http://coq.inria.fr/
-   Bytecode VM enabled         : true
-   Native Compiler enabled     : no
-
-   Paths where installation is expected by Coq Makefile:
-   - Coq is expected in /home/hiroki/.opam/default
-   - the Coq library is expected in /home/hiroki/.opam/default/lib/coq
-   - the Coqide configuration files is expected in /home/hiroki/.opam/default/etc/xdg/coq
-   - the Coqide data files is expected in /home/hiroki/.opam/default/share/coq
-   - the Coq man pages is expected in /home/hiroki/.opam/default/man
-   - documentation prefix path for all Coq packages is expected in /home/hiroki/.opam/default/share/doc
-
- If anything is wrong above, please restart './configure'.
-
- *Warning* To compile the system for a new architecture
-           don't forget to do a 'make clean' before './configure'.
λ compiled  coqide-server.8.17.1
 installed coqide-server.8.17.1
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "make" "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coq-stdlib.8.17.1)
- dune build  --root . theories_dune ltac2_dune
- touch .dune-stamp
- cp -a _build/default/theories_dune theories/dune && chmod +w theories/dune
- cp -a _build/default/ltac2_dune user-contrib/Ltac2/dune && chmod +w user-contrib/Ltac2/dune
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "dune" "build" "-p" "coq-stdlib" "-j" "7" "@install" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coq-stdlib.8.17.1)
λ compiled  coq-stdlib.8.17.1
 installed coq-stdlib.8.17.1
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "dune" "build" "-p" "coq" "-j" "7" "@install" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coq.8.17.1)
λ compiled  coq.8.17.1
 installed coq.8.17.1
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "dune" "build" "-p" "coq-serapi" "-j" "7" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coq-serapi.8.17.0+0.17.0)
λ compiled  coq-serapi.8.17.0+0.17.0
 installed coq-serapi.8.17.0+0.17.0
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "dune" "subst" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coqfmt.0.1.0)
+ /home/hiroki/.opam/opam-init/hooks/sandbox.sh "build" "dune" "build" "-p" "coqfmt" "-j" "7" "@install" (CWD=/home/hiroki/.opam/default/.opam-switch/build/coqfmt.0.1.0)
λ compiled  coqfmt.0.1.0
 installed coqfmt.0.1.0
Done.

view this post on Zulip Paolo Giarrusso (Sep 17 2023 at 20:18):

that's 8.17.1 but it also uses zarith, so that doesn't seem the problem...

view this post on Zulip Michael Soegtrop (Sep 18 2023 at 07:06):

@Hiroki Tokunaga : if you have a day or two, I could provide a basic Coq Platform pick for Coq 8.10 and a more complete one for Coq 8.11. Currently Coq Platform goes back to 8.12. I asked a while back if there is interest in older versions and there was none, but I expected that some day someone wants to reproduce some 8.10 artifacts.

view this post on Zulip Théo Zimmermann (Sep 18 2023 at 08:26):

Not sure that I can see the link between this question and Coq 8.10 / 8.11.

view this post on Zulip Michael Soegtrop (Sep 18 2023 at 09:48):

@Théo Zimmermann : sorry I should wear my glasses - on the fly I read 8.18.0 as 8.10.0.

view this post on Zulip Théo Zimmermann (Sep 18 2023 at 09:50):

OK. IMO, the more time passes, the less likely it becomes that someone will need an 8.10/8.11-based Coq Platform.


Last updated: Jun 13 2024 at 19:02 UTC