Alperen Keles (Feb 15 2023 at 20:59): 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
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.
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
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?
Gaëtan Gilbert (Feb 15 2023 at 23:04):the error is located in c code so it does have c code
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.
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?
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?
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.
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).
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?
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.
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.
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
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.
Michael Soegtrop (Mar 02 2023 at 09:27):Can someone on NIX please post the "Global opam variables" part of opam var for NIX?
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 ...
Théo Zimmermann (Mar 02 2023 at 09:29):I'm unsure I understand your request.
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.
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.
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.
Michael Soegtrop (Mar 02 2023 at 09:31):I still would be interested to know what opam var looks like on NIX.
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
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).
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.
Michael Soegtrop (Mar 02 2023 at 09:35):Btw.: would it be hard to implement it?
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.
Michael Soegtrop (Mar 02 2023 at 10:00):I see - I guess one has to try it once to understand the implications.
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.
Michael Soegtrop (Mar 02 2023 at 10:09):(we need pkg-config anyway elsewhere)
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.
Michael Soegtrop (Mar 03 2023 at 08:33):OK, I will keep the manual OS dependent builds then.
Last updated: Sep 23 2023 at 07:01 UTC