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 21:17:10 -0600 Message-ID: <877e25xoi1.fsf@gnu.org> References: <87imlpy07j.fsf@gnu.org> <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Return-path: Received: from eggs.gnu.org ([2001:470:142:3::10]:53067) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioIu3-00019f-Ad for bug-guix@gnu.org; Sun, 05 Jan 2020 22:18:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioIu2-000388-Bs for bug-guix@gnu.org; Sun, 05 Jan 2020 22:18:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38908) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioIu2-000383-8y for bug-guix@gnu.org; Sun, 05 Jan 2020 22:18:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioIu2-00034o-3r for bug-guix@gnu.org; Sun, 05 Jan 2020 22:18:02 -0500 Sender: "Debbugs-submit" Resent-Message-ID: In-Reply-To: <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> (Julien Lepiller's message of "Sun, 05 Jan 2020 18:19:10 -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: Julien Lepiller Cc: bandali@gnu.org, 38959@debbugs.gnu.org Julien Lepiller writes: > Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio a =C3= =A9crit : >>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. > > We don't have too many coq packages, so when updating coq I've always > built them all and checked they were ok. I think coq 8.10 was released > for enough time for upstream to update their code base. We should give > it a try. I can work on this tomorrow and report my findings if you > like. Or you could take care of it if you prefer :) > > I'd prefer to have only one version of coq in guix, but if we need two of= them, so be it. Let's make sure we duplicate other coq packages in that ca= se. > I should have some time tonight. I will give it a shot and open a patch series, and report back the bug number here. :) --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]