coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Coq Club <coq-club AT inria.fr>
Cc: Benedikt Ahrens <benedikt.ahrens AT gmail.com>
Subject: Re: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable
Date: Thu, 25 Feb 2021 16:40:31 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Pierre.Courtieu AT cnam.fr; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f171.google.com
Ironport-phdr: 9a23:2AxlsR+v8OYm+/9uRHKM819IXTAuvvDOBiVQ1KB20u4cTK2v8tzYMVDF4r011RmVBNSdu6IP1beempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgFFiCC+bL5xIxm7rAXcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/9KpgVgPmhzkbOD446GHXi9J/jKRHoBK6uhdzx5fYbJyJOPZie6/Qe84RS2hcUcZLTyFODY28YIkPAeQPPuhWspfzqEcVoBSkGQWhHvnixiNUinL026AxzuQvERvB3AwlB98AqnXUo8vvNKcIT+++0bfFzTLeb/NMxTf96ZbHcg08qvyLR7xwcNTeyVM1FwzblFmdt4vlPy6P1uQRsmiU8fdgWPmzhG4hsQ5xpyKjxsk2ioTQgI8e11/L+zljzokvOd24VFB0YcSiEJZIuC+XKZV7T94tTm12tig3zr4LtJG7ciUIyJkqxwDTZ+GJfoSW/h7uSOKcLSt2inxldryymxe//0aix+DyVsS60FBHpTdLnNnLs3ACzR3T6s6fR/ty/0ehxTaP1x3I5e1ePU80kq/bJpg8ybAzjpoeqVrPEjPylUnsj6Kbdl8o9vWp5unmeLnqu52RO5JyhwrjKKohgNa/Dv49MgUWX2iU5+C81Lr78E38WrpKj/k2nrDYsJDeOMgXv6C5DxJX34o+8Rq/ADCm0NMXnXkDMl1JYg6Ij4/sO13WIfD4C+mwg0i0nTt12/zLOqftD5bNI3TZjbvsfLdw51RBxAcx0NxT/5dUBasAIPL3VE/xrtvYDhohPgyswuboFs991pkAVm6VHqCZN77SsUWU5uIuPeaMeZQYuDn4K/c/5v7uiWU1lkMafamsxZcXcmy3Hux6I0WFZnrhmssOEWATvgYnUOPqjECCXiVIanapX6M84yk7B5i8AYfCQICtmr2B0z2hEp1YfGAVQmyLRFzvbs2vX+oGIHaZJdYkmTgZX5CgTZUg3Fegrlmp5aBgK7/s+yACr5+r/99o/fHSmAx6oQR1At6H3iemSHxugmIFWhc92ql650JnnATQmZNkiuBVQIQAr8hCVR03YNuFl7QjVoLCHznZd9LMc26IB9WrBTZrEIA0yt4KJkd5QpCs10+amSWtBLARmvqAA5lmqvuNjUi0HN50zjP97IdkilAnRsVVMmj/3/xw8gHSA8jClEDLzv/2J5RZ5zbE8SK49UTLpFtRAVx7V6zAG34FNBPb

Hi, I tend to do:

opam init

opam install coq

opam remove coq

This leaves my system with everything needed to compile coq. And indeed zarith 1.11 is installed with opam.

Hope this helps.

Pierre

Le jeu. 25 févr. 2021 à 15:34, Michael Soegtrop <MSoegtrop AT yahoo.de> a écrit :

Hi Benedikt,

did you give the Coq Platform setup scripts a try? For the 8.13.1
version and Linux the instructions are here:

https://github.com/coq/platform/blob/2021.02/README_Linux.md

There is a snap package and an opam based fully automated "compile from
sources" method - the scripts will also setup opam in case it is not yet
there and install system prerequisites as needed.

The scripts did work last time I tried it on Debian (it compiles ZArith
from sources using opam).

Best regards,

Michael

[Coq-Club] Zarith - compiling Coq 8.13 on Debian stable, Benedikt Ahrens, 02/25/2021
- Re: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable, Michael Soegtrop, 02/25/2021
  - Re: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable, Pierre Courtieu, 02/25/2021
    - Re: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable, Xavier Leroy, 02/25/2021