coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Michael Soegtrop <MSoegtrop AT yahoo.de>
To: coq-club AT inria.fr, Benedikt Ahrens <benedikt.ahrens AT gmail.com>
Subject: Re: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable
Date: Thu, 25 Feb 2021 15:34:02 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=MSoegtrop AT yahoo.de; spf=Pass smtp.mailfrom=msoegtrop AT yahoo.de; spf=None smtp.helo=postmaster AT sonic312-23.consmr.mail.ne1.yahoo.com
Ironport-phdr: 9a23:5Zls1B310/oIS/WhsmDT+DRfVm0co7zxezQtwd8ZseMTLvad9pjvdHbS+e9qxAeQG9mCurQU26GI7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVgDexe7B/IRa5oQjQtsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LpwRRT2lCkIKSI28GDPisxxkq1bpg6hpwdiyILQeY2ZKeZycr/Ycd4cWGFPXNteVzZZD42hcYUPAeoPM+VWoYbzqFQBrwexCwarCu701j9FhGX70bEg3ukvEwzL2hErEdIUsHTTqdX4LKAcUeGpw6nI1zrMcfdW0irg5ojPbB8hru2MXah3ccrJ1EIiEATLgEiXqYP7MDOVyv4Ns2+D7+d7VeOgkW4nqwZ2ojS128gjlJDEi4QIwV/L6St32pw6JcGkSEFle96kFoNdui6VOoZ4Rs4uX3xktiknxrMGpJO2fSgHxZonyhPCZPGJfYqF7BLtWeuRLjl0mWxodbCiixu28kWuyunxW8qp3VtMsyFLnN7MtnUX2BzS7MiKUvR9/ka92TaPygDc8ftILlwzlareLZMq370+loILvEnCHyL6glj6ga6Ye0k+5+Sl7/nrbq/4qpOAOIJ5jBz1PL40lcylG+s4NxADX2iF9uS4073u5Vb5QLJMjv03jqbUvo3WKdoCqqKnDQJZyJos6xG5Dze91dQYh2MLLFdfdxKGi4jlIVfOL+7lAfulg1Wjijdrx/fBPrH7HprNKX3DnK/gfbZ79UFc1BI+wNFe6p5OF70MIfz+VlXsuNHcExM1KRK4z/roBdll04MRQ2OPAquXMKPItl+I4/oiI+yXZI8Spjn9JOQl5+TpjX8hglIcfbOm3ZsQaHC/BPhpPluWbWL2gtgdCWcKohY+TOvyhVKeVj5Tfm++UL445jEmE42rFpzDR4CogLyZxii3BJxWZmZcClCNC3jkbYuEW+1fIB6Vd8Rmi3kPUaWrY44nzxCn8gHgj/JNI+zZ9iwbqdrK1MJ44fabwRs/8zF4DseBlWiNVWxyhUsHQjY32OZ0pkkrmXmZ1q0tpv1TFdVe47tyVQo1KYTb16QuLuv1Vw3dZNCRYEevQtKhRz08GIFii+QSalpwTo3xxivI2DCnVvpMz+TSWM4Et5nE1n20HP5Tjm7c3fB53UgvQsxIc2Gr1PYmqlrjQrXRmkDcrJ6EMKQR2CmWpTWYymyPtxoBCksqCuPOWnYEY1GQqN344gXEQuboGL0nNQwHwsmHePMTO4/ZyG5eTfKmA+zwJme4mmO+HxGNn+vefYPqfGJb0CiPUUU=

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