# Error while installing Coq platform

**URL:** <https://discourse.rocq-prover.org/t/error-while-installing-coq-platform/1234>\
**Category:** Using Rocq\
**Created:** [March 17, 2021, 5:33am UTC](https://discourse.rocq-prover.org/t/error-while-installing-coq-platform/1234 "2021-03-17T05:33:55Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![LouGlzHuesca](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/louglzhuesca/32/189_2.png) [@LouGlzHuesca](https://discourse.rocq-prover.org/u/LouGlzHuesca)\
**Post date:** [March 17, 2021, 5:33am UTC](https://discourse.rocq-prover.org/t/error-while-installing-coq-platform/1234/1 "2021-03-17T05:33:55Z")

</div>

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](https://github.com/coq/platform/blob/2021.02/README_Linux.md#installation-by-compiling-from-sources-using-opam)  
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](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!

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [March 18, 2021, 12:01pm UTC](https://discourse.rocq-prover.org/t/error-while-installing-coq-platform/1234/2 "2021-03-18T12:01:20Z")

</div>

Hi Lourdes 👋

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](https://github.com/ocaml/opam/issues/3692)) 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.

---

<div class="post-metadata">

**Author:** ![LouGlzHuesca](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/louglzhuesca/32/189_2.png) [@LouGlzHuesca](https://discourse.rocq-prover.org/u/LouGlzHuesca)\
**Post date:** [March 18, 2021, 4:28pm UTC](https://discourse.rocq-prover.org/t/error-while-installing-coq-platform/1234/3 "2021-03-18T16:28:57Z")

</div>

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](https://github.com/ocaml/Zarith/issues/77)  
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!