coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Benedikt Ahrens <benedikt.ahrens AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Zarith - compiling Coq 8.13 on Debian stable
Date: Thu, 25 Feb 2021 14:36:59 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=benedikt.ahrens AT gmail.com; spf=Pass smtp.mailfrom=benedikt.ahrens AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f42.google.com
Ironport-phdr: 9a23:HDs+8BFXQ4ABHcJoqfMF1p1GYnF86YWxBRYc798ds5kLTJ7yp86wAkXT6L1XgUPTWs2DsrQY0ruQ4/CrBzFIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLd/IA+1oAjSucUbgItvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFojKxVvQyvqR9xzYHab46aKPVwc7jBfd4YX2dNQtpdWiJDD466coABD/ABPeFdr4TlulYBsx2+ChexC+PuyT9ImmL90LE60+Q7Dw7G2hcgFM8JvXvPstr1MrkdXv20zKnL0TXPdelZ2Tfn6IfWdBAhuuqBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvGeH4eR6T+2vl3InpB9rojip3soglobHi4AUx1zZ9Sh0wYY7KN23RkJmb9OpDZVeuj2UOodqQM4sTWFmtSUmx7MJu5O2ficExIooyhPddvCLbYqF7xT+X+iSOTd1nGxpdK67ihqo8kWtyvfwWtSq3FtJtCZIncfAumgT2xDP9sSLV/5w8V2g1DqS0g3f9+9JLEAqmqfeJJMu3KI8mocWvEjeHiL7mUb7gaqIeUo65+Sn9+Hqbqv9qZOCNIJ5jwPzP6o0lcG9B+kzLxIAUHKB+eum0b3u5U35T6tOjv0xiqTZtYrVJcUfpqKgDQ5V15sv5w+xDzqpztgUh3YHLFVCeBKIi4jmJUvCL+z/Dfe6m1iskTFryO7aPrD5HJnBMnzOnK3icLt98UJQ1RQ/wNNF659bFL0NOPfzVVXwtNzcAB85KQu0w+P/BdpmyIweX3yADbKYMKPRrV+E/PggI+mWZIALvjb9MOMo5/HrjXAjmF8debOl0ocQaHC9BvhmOVmWYWLwgtcdFmcHphYxTOvziFGbTTFTY2uyULkn6zEgCIOmCJ/DSZq3jLyA2ie7BJxWaXpcBlCCC3e7P7mDDvwLcWeZJtJruj0CT7moDYE7hj+0swqv4bdhI+bV+TFQnJL52d5ur7nZmBc/+T13E4KU03uASXpckWYBRjtw16d69x8ugmyf2LR11qQLXedY4OlEB19jaMzsitdiAtW3YTrvO9eETFH8H4ejCDA1C800mpoAPxw7FNKlgRTOmSGtBu1Nzu3ZNNkP6qvZmkPJCYN4wnfC2rMmigB/EMRKPGyiwKV48lqKXtKbowCij6+vMJ8k8mvV7m7alDiBuUhZVEh7VqCXBX0=

Hi,

Coq 8.13 is telling me that it requires Zarith version 1.10. In Debian stable, only 1.7 is available.

Is there a way to compile Coq 8.13 with Zarith 1.7, even if that meant sacrificing some functionality, or taking a performance hit?

Side remarks:
- The configure script tells me that my Zarith version is 1.5, whereas apt tells me that it is 1.7.
- Ubuntu 20.04 seems to ship Zarith 1.9, but there Coq 8.13 compiles fine (according to a report by someone else).

Thanks for any advice!
Benedikt

[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