Error while installing Coq platform

Using Coq
1

Hi everyone,

I am trying to install the last version of Coq (8.13.1) using the Coq Platform under Linux Mint 19 Cinnamion, following the instructions here platform/README_Linux.md at 2021.02 · coq/platform · GitHub
I used to install Coq from source and I have already cleaned by computer from old versions and files.
I had encountered several issues that I have already solved but I can’t manage to get a clean installation.

The error I have is the following:
Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build conf-gmp 3
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install conf-findutils 1
│ ∗ install num 1.4
│ ∗ install ocamlfind 1.9.1
└─

giving me the fatal error

/home/lou/.opam/log/conf-gmp-5672-8b8a2d.info
1 # context 2.0.8 | linux/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#8b0c6c8d
2 # path ~/.opam/coq-platform.2021.02.0/.opam-switch/build/conf-gmp.3
3 # command ~/.opam/opam-init/hooks/sandbox.sh build sh -exc cc -c $CFLAGS -I/usr/local/include test.c
4 # env-file ~/.opam/log/conf-gmp-5672-8b8a2d.env
5 # output-file ~/.opam/log/conf-gmp-5672-8b8a2d.out
/home/lou/.opam/log/conf-gmp-5672-8b8a2d.out
1 + cc -c -I/usr/local/include test.c
2 test.c:1:10: fatal error: gmp.h: No such file or directory
3 #include <gmp.h>
4 ^~~~~~~
5 compilation terminated.

I also made

opam update
opam install conf-gmp

having the same error.

Could someone point me to a piece of advice to solve this?
Thanks in advance!

2

Hi Lourdes :wave:

The Coq platform scripts rely on opam-depext to install external dependencies (in this case, you need gmp, which is not installed on your system and this is why installing conf-gmp fails). It looks like opam-depext doesn’t support Linux Mint properly (Linux Mint support · Issue #3692 · ocaml/opam · GitHub) but a workaround is simply to replace ID=linuxmint with ID=ubuntu and ID_LIKE=ubuntu with ID_LIKE=debian in /etc/os-release. Another (less invasive) solution in your case would be installing gmp manually (sudo apt install libgmp-dev) although you might face this issue again for other external dependencies.

3

Thanks Théo.

As you pointed, I haven’t installed gmp.
I was looking for some answers on the web and I found some hints in the issues of OCaml, in particular, gmp.h not found when compiling with `4.11.1+musl+static+flambda` · Issue #77 · ocaml/Zarith · GitHub
Hence I tried to install libgmp* as the installation only of libgmp-dev was not enough.
With this, I finally have Coq and coqide installed!

Hope this could help others while installing Coq using the platform.

Greetings from Mexico!

1 Like