Stream: Coq users

Topic: Error When Installing Coq from OPAM(RHEL 8.7)


view this post on Zulip Alperen Keles (Feb 15 2023 at 20:59):

I am working in Red Hat Enterprise Linux 8.7

I have installed opam as a binary, I have opam version 2.1.4. I tried two switches, 4.10.2+afl and 4.11.2+afl and I am getting the same error in both. My coq version is 8.15.2.

[ERROR] The compilation of coq.8.15.2 failed at "make COQ_USE_DUNE= -j35".

#=== ERROR while compiling coq.8.15.2 =========================================#
# context     2.1.4 | linux/x86_64 | ocaml-variants.4.11.2+afl | pinned(https://github.com/coq/coq/archive/refs/tags/V8.15.2.tar.gz)
# path        ~/.opam/4.11.2+afl/.opam-switch/build/coq.8.15.2
# command     ~/.opam/opam-init/hooks/sandbox.sh build make COQ_USE_DUNE= -j35
# exit-code   2
# env-file    ~/.opam/log/coq-185234-20c0a1.env
# output-file ~/.opam/log/coq-185234-20c0a1.out
### output ###
# [...]
# /home/akeles/.opam/4.11.2+afl/lib/zarith/libzarith.a(caml_z.o): In function `ml_z_fac2':
# caml_z.c:(.text+0xbacf): undefined reference to `mpz_2fac_ui'
# /home/akeles/.opam/4.11.2+afl/lib/zarith/libzarith.a(caml_z.o): In function `ml_z_facM':
# caml_z.c:(.text+0xbbee): undefined reference to `mpz_mfac_uiui'
# /home/akeles/.opam/4.11.2+afl/lib/zarith/libzarith.a(caml_z.o): In function `ml_z_primorial':
# caml_z.c:(.text+0xbccf): undefined reference to `mpz_primorial_ui'
# collect2: error: ld returned 1 exit status
# File "caml_startup", line 1:
# Error: Error during linking (exit code 1)
# make[1]: *** [Makefile.common:130: _build/install/default/bin/coqproofworker.opt] Error 1
# make[1]: Leaving directory '/home/akeles/.opam/4.11.2+afl/.opam-switch/build/coq.8.15.2'
# make: *** [Makefile.make:122: submake] Error 2

view this post on Zulip Karl Palmskog (Feb 15 2023 at 21:00):

it looks like you haven't installed the GMP library in your OS package manager. This means that the Coq dependency zarith will fail to work. So it's not directly related to Coq.

view this post on Zulip Paolo Giarrusso (Feb 15 2023 at 22:45):

Possibly, but isn't it somewhat impressive that zarith built without GMP and Coq's build got that far? But maybe having part of the gmp package would do it... that error mentions static library libzarith.a, which will need gmp's static library, which is likely to need a package like libgmp-dev

view this post on Zulip Paolo Giarrusso (Feb 15 2023 at 22:47):

The failure seems still strange, since I'd expect libgmp C headers to live in libgmp-dev as well. Maybe zarith can build without those headers because it has no C code?

view this post on Zulip Gaëtan Gilbert (Feb 15 2023 at 23:04):

the error is located in c code so it does have c code

view this post on Zulip Guillaume Melquiond (Feb 16 2023 at 10:02):

Are there other functions from GMP missing or are those the only three? (Hard to tell from the log truncated by Opam.) The reason I am asking is that these three generalized factorials are a somewhat recent addition to GMP (10 years ago) and even more recent for Mini-GMP (less than one year ago). So, if RHEL ships an old version of GMP, or if it substitutes Mini-GMP to GMP, this might explain the issue.

view this post on Zulip Michael Soegtrop (Feb 17 2023 at 10:23):

We should review if GMP is covered for RHEL in the opam file:

https://github.com/ocaml/opam-repository/blob/master/packages/conf-gmp/conf-gmp.4/opam

On first glance it doesn't look like it.

@Alperen Keles : can you please post the "Global opam variables" part of opam var?

view this post on Zulip Michael Soegtrop (Feb 17 2023 at 10:24):

@Guillaume Melquiond : can you please check if the tests in

https://github.com/ocaml/opam-repository/blob/master/packages/conf-gmp/conf-gmp.4/files/test.c

would pass if the requirements of Coq are fulfilled?

view this post on Zulip Michael Soegtrop (Feb 17 2023 at 10:27):

All in all opam should handle system dependencies automatically since the full integration of depext (2.1?), and if it doesn't it is a bug (or non feature) in the opam files.

view this post on Zulip Guillaume Melquiond (Feb 17 2023 at 13:18):

As far as I can tell from https://github.com/ocaml/opam-repository/blob/master/packages/conf-gmp/conf-gmp.4/opam, they do not try to link the resulting files. So, it will not fail if the archive files are missing (as long as the header files are present).

view this post on Zulip Michael Soegtrop (Feb 17 2023 at 17:50):

@Guillaume Melquiond So one should add a main function to "test.c" and remove the "-c" flag in the compilation? Are the 3 functions called sufficient to conclude that the installed GMP is likely OK?

view this post on Zulip Guillaume Melquiond (Feb 17 2023 at 18:02):

Yes, it should be fine. (I was worried that they might be macros, but no, they are actual functions.)
More precisely, you need to change void test(void) into int main(), you need to remove -c from the command line, and you need to add -lgmp.

view this post on Zulip Michael Soegtrop (Feb 20 2023 at 08:42):

@Alperen Keles (or anybody who has a Red Hat Enterpreise Linux installation with opam) : can you please post the "Global opam variables" part of opam var? I then can do a PR to fix the opam package.

view this post on Zulip Alperen Keles (Feb 27 2023 at 18:19):

<><> Global opam variables ><><><><><><><><><><><><><><><><><><><><><><><><><><>
arch              x86_64             # Inferred from system
exe                                  # Suffix needed for executable filenames (Windows)
jobs              35                 # The number of parallel jobs set up in opam configuration
make              make               # The 'make' command to use
opam-version      2.1.4              # The currently running opam version
os                linux              # Inferred from system
os-distribution   rhel               # Inferred from system
os-family         fedora             # Inferred from system
os-version        8.7                # Inferred from system
root              /home/akeles/.opam # The current opam root directory
switch            4.11.2+afl         # The identifier of the current switch
sys-ocaml-arch                       # Target architecture of the OCaml compiler present on your system
sys-ocaml-cc                         # Host C Compiler type of the OCaml compiler present on your system
sys-ocaml-libc                       # Host C Runtime Library type of the OCaml compiler present on your
                                       system
sys-ocaml-version                    # OCaml version present on your system independently of opam, if any

@Michael Soegtrop I pasted it above

view this post on Zulip Michael Soegtrop (Feb 28 2023 at 08:29):

@Alperen Keles : thanks!

One note on your settings: jobs=35 is very likely to fail on larger opam requests unless you have 256 GB RAM or so. The job count is used by both opam to see how many builds to start in parallel and by the individual builds as -j option to make, so the effect is at times quadratic.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:27):

Can someone on NIX please post the "Global opam variables" part of opam var for NIX?

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:29):

Does someone know if opam is aware that NIX exists? Looking at opam src I guess it doesn't ...

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:29):

I'm unsure I understand your request.

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:30):

If you are talking about Nix / NixOS, then opam is only aware of the existence of NixOS to tell that the automatic depext installation process is not supported on NixOS.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:30):

@Théo Zimmermann : I need the output of the command opam var for an opam installed on NIX.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:30):

I see. I am looking at the conf-gmp package and it has some nixos specific stuff in it, which I concluded cannot possibly work.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:31):

I still would be interested to know what opam var looks like on NIX.

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:32):

<><> Global opam variables ><><><><><><><><><><><><><><><><><><><><><><><><><><>
arch              x86_64           # Inferred from system
exe                                # Suffix needed for executable filenames (Windows)
jobs              7                # The number of parallel jobs set up in opam configuration
make              make             # The 'make' command to use
opam-version      2.1.4            # The currently running opam version
os                linux            # Inferred from system
os-distribution   nixos            # Inferred from system
os-family         nixos            # Inferred from system
os-version        22.11            # Inferred from system
root              /home/theo/.opam # The current opam root directory
switch                             # The identifier of the current switch
sys-ocaml-arch                     # Target architecture of the OCaml compiler present on your system
sys-ocaml-cc                       # Host C Compiler type of the OCaml compiler present on your system
sys-ocaml-libc                     # Host C Runtime Library type of the OCaml compiler present on your
                                     system
sys-ocaml-version                  # OCaml version present on your system independently of opam, if any

<><> Configuration variables from the current switch ><><><><><><><><><><><><><>
No switch installed

<><> Package variables ('opam var --package PKG' to show) <><><><><><><><><><><>
PKG:name       # Name of the package
PKG:version    # Version of the package
PKG:depends    # Resolved direct dependencies of the package
PKG:installed  # Whether the package is installed
PKG:enable     # Takes the value "enable" or "disable" depending on whether the package is installed
PKG:pinned     # Whether the package is pinned
PKG:bin        # Binary directory for this package
PKG:sbin       # System binary directory for this package
PKG:lib        # Library directory for this package
PKG:man        # Man directory for this package
PKG:doc        # Doc directory for this package
PKG:share      # Share directory for this package
PKG:etc        # Etc directory for this package
PKG:build      # Directory where the package was built
PKG:hash       # Hash of the package archive
PKG:dev        # True if this is a development package
PKG:build-id   # A hash identifying the precise package version with all its dependencies
PKG:opamfile   # Path of the curent opam file

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:34):

FWIW, this is opam installed with Nix on NixOS. There also exist the possibility of installing opam with Nix outside NixOS (but this has probably no valid use case as of today).

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:35):

As far as I can see - and as you said - opam does not handle os-family=nixos (the word nixos does not occur in the respective file). So I will remove the nixos entry from conf-gmp.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 09:35):

Btw.: would it be hard to implement it?

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:43):

When the required depext is an executable, it wouldn't be too difficult to make opam call nix-env to install it. However, this would probably be unsatisfying because NixOS users do not like installing packages globally in a non-declarative way like this. Furthermore, this would not work for depext libraries (like gmp I suppose), because even if they are installed with nix-env, the packages that need them wouldn't find them where they expect them. The usual solution to install libraries and have the tools that need them locate them is to drop into a nix-shell because it will make the environment aware of the libraries using environment variables. For instance, when I create a new switch with opam, I do so inside nix-shell -p binutils. If I need to build CoqIDE, then I probably need a nix-shell -p gtksourceview or something like this (it's been a long time that I haven't tried). This is still not perfect, because if I later garbage-collect my Nix store, it is likely that the needed libraries will be removed and that this will break any program that needs to load them dynamically.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 10:00):

I see - I guess one has to try it once to understand the implications.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 10:02):

@Guillaume Melquiond : since the test build instructions in conf-gmp are a bit OS dependent, I wonder if I shouldn't just do "pkg-config --exists gmp" instead. This should be reasonably safe and less contrived than the current code.

view this post on Zulip Michael Soegtrop (Mar 02 2023 at 10:09):

(we need pkg-config anyway elsewhere)

view this post on Zulip Guillaume Melquiond (Mar 02 2023 at 15:12):

Michael Soegtrop said:

Guillaume Melquiond : since the test build instructions in conf-gmp are a bit OS dependent, I wonder if I shouldn't just do "pkg-config --exists gmp" instead. This should be reasonably safe and less contrived than the current code.

Unfortunately, hardly anyone uses pkg-config for GMP (e.g., zarith does not, which is the main user of conf-gmp in the Opam world). So, if pkg-config answers that GMP is installed but it is installed in a non-standard location, everything will break later.

view this post on Zulip Michael Soegtrop (Mar 03 2023 at 08:33):

OK, I will keep the manual OS dependent builds then.


Last updated: Jun 25 2024 at 15:02 UTC