From mboxrd@z Thu Jan 1 00:00:00 1970 From: Julien Lepiller Subject: bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums Date: Sun, 05 Jan 2020 18:19:10 -0500 Message-ID: <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> References: <87imlpy07j.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]:53607) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioFBl-0002vK-V9 for bug-guix@gnu.org; Sun, 05 Jan 2020 18:20:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioFBj-0005bi-CJ for bug-guix@gnu.org; Sun, 05 Jan 2020 18:20:04 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:38817) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ioFBi-0005bP-KQ for bug-guix@gnu.org; Sun, 05 Jan 2020 18:20:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ioFBi-0005HZ-Ei for bug-guix@gnu.org; Sun, 05 Jan 2020 18:20:02 -0500 Sender: "Debbugs-submit" Resent-Message-ID: Received: from eggs.gnu.org ([2001:470:142:3::10]:53588) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ioFBB-0002sV-AK for bug-guix@gnu.org; Sun, 05 Jan 2020 18:19:30 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ioFBA-0005Oj-8T for bug-guix@gnu.org; Sun, 05 Jan 2020 18:19:29 -0500 In-Reply-To: <87imlpy07j.fsf@gnu.org> 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: brettg@gnu.org, 38959@debbugs.gnu.org Cc: bandali@gnu.org Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio a =C3= =A9crit : >Hey all, and particularly the FM-Guix working group=2E I'd like to get >Coq >8=2E10=2E1 into Guix as it provides support for the new Int63=2ERing63 th= eory >number library=2E This would be immensely helpful in getting the >coq-bignums package up-to-date with some neat new tactics=2E I know that >the CoqIDE package now has an explicit dependency on lablgtk3 from >OCaml=2E Both Coq 8=2E10=2E1 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=2E > >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=2E So we very well may have to >make the newer Coq along side an existing version=2E > >That's all, let me know what you think=2E We don't have too many coq packages, so when updating coq I've always buil= t them all and checked they were ok=2E I think coq 8=2E10 was released for = enough time for upstream to update their code base=2E We should give it a t= ry=2E I can work on this tomorrow and report my findings if you like=2E 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=2E Let's make sure we duplicate other coq packages in that c= ase=2E