From mboxrd@z Thu Jan 1 00:00:00 1970 From: Brett Gilio Subject: bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums Date: Sun, 05 Jan 2020 17:04:16 -0600 Message-ID: <87imlpy07j.fsf@gnu.org> Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:51691) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioExG-00063Y-FS for bug-guix@gnu.org; Sun, 05 Jan 2020 18:05:07 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioExC-0001E3-Qt for bug-guix@gnu.org; Sun, 05 Jan 2020 18:05:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38811) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioExC-0001Do-Lk for bug-guix@gnu.org; Sun, 05 Jan 2020 18:05:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioExC-0004tv-Fx for bug-guix@gnu.org; Sun, 05 Jan 2020 18:05:02 -0500 Sender: "Debbugs-submit" Resent-Message-ID: Received: from eggs.gnu.org ([2001:470:142:3::10]:51578) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioEwU-00060Y-1p for bug-guix@gnu.org; Sun, 05 Jan 2020 18:04:19 -0500 List-Id: Bug reports for GNU Guix List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-guix-bounces+gcggb-bug-guix=m.gmane.org@gnu.org Sender: "bug-Guix" To: 38959@debbugs.gnu.org Cc: bandali@gnu.org Hey all, and particularly the FM-Guix working group. I'd like to get Coq 8.10.1 into Guix as it provides support for the new Int63.Ring63 theory number library. This would be immensely helpful in getting the coq-bignums package up-to-date with some neat new tactics. I know that the CoqIDE package now has an explicit dependency on lablgtk3 from OCaml. Both Coq 8.10.1 and lablgtk3 exist on Julien's (cc) channel, but I want to run the idea by Julien and others before possibly integrating a new Coq into our repository. We should be extra cautious when doing this, as there is quite possibly some Coq packages that /do not/ run against coqtop from a newer Coq version. So we very well may have to make the newer Coq along side an existing version. That's all, let me know what you think. -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]