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: Mon, 06 Jan 2020 02:39:44 -0600 Message-ID: <8736ctvuzz.fsf@gnu.org> References: <87imlpy07j.fsf@gnu.org> <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> <877e25xoi1.fsf@gnu.org> 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]:45217) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioNvf-0005DH-PW for bug-guix@gnu.org; Mon, 06 Jan 2020 03:40:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioNve-0007Zb-I5 for bug-guix@gnu.org; Mon, 06 Jan 2020 03:40:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:39019) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioNve-0007ZN-Ep for bug-guix@gnu.org; Mon, 06 Jan 2020 03:40:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioNve-0003MX-CK for bug-guix@gnu.org; Mon, 06 Jan 2020 03:40:02 -0500 Sender: "Debbugs-submit" Resent-To: bug-guix@gnu.org Resent-Message-ID: In-Reply-To: <877e25xoi1.fsf@gnu.org> (Brett Gilio's message of "Sun, 05 Jan 2020 21:17:10 -0600") 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: 38959-done@debbugs.gnu.org, bandali@gnu.org Brett Gilio writes: > 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 o= f them, so be it. Let's make sure we duplicate other coq packages in that c= ase. >> > > I should have some time tonight. I will give it a shot and open a patch > series, and report back the bug number here. :) Moving conversation to bugs.gnu.org/38965. Closing. --=20 Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]