From unknown Sat Aug 09 13:07:06 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#38959 <38959@debbugs.gnu.org> To: bug#38959 <38959@debbugs.gnu.org> Subject: Status: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums Reply-To: bug#38959 <38959@debbugs.gnu.org> Date: Sat, 09 Aug 2025 20:07:06 +0000 retitle 38959 Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums reassign 38959 guix submitter 38959 Brett Gilio severity 38959 normal thanks From debbugs-submit-bounces@debbugs.gnu.org Sun Jan 05 18:04:22 2020 Received: (at submit) by debbugs.gnu.org; 5 Jan 2020 23:04:22 +0000 Received: from localhost ([127.0.0.1]:44784 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioEwX-0004sv-Gw for submit@debbugs.gnu.org; Sun, 05 Jan 2020 18:04:21 -0500 Received: from lists.gnu.org ([209.51.188.17]:48698) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioEwV-0004sn-AF for submit@debbugs.gnu.org; Sun, 05 Jan 2020 18:04:20 -0500 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 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-2.9 required=5.0 tests=ALL_TRUSTED,BAYES_00, URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:470:142:3::e]:45066) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioEwT-0000ar-6c; Sun, 05 Jan 2020 18:04:17 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=45366 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioEwR-0004zx-HN; Sun, 05 Jan 2020 18:04:16 -0500 From: Brett Gilio To: bug-guix@gnu.org Subject: 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 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: submit Cc: julien@lepiller.eu, bandali@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) 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] From debbugs-submit-bounces@debbugs.gnu.org Sun Jan 05 18:19:33 2020 Received: (at submit) by debbugs.gnu.org; 5 Jan 2020 23:19:33 +0000 Received: from localhost ([127.0.0.1]:44790 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioFBF-0005Gn-3s for submit@debbugs.gnu.org; Sun, 05 Jan 2020 18:19:33 -0500 Received: from lists.gnu.org ([209.51.188.17]:39649) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioFBC-0005Ge-Bq for submit@debbugs.gnu.org; Sun, 05 Jan 2020 18:19:32 -0500 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 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=BAYES_40,URIBL_BLOCKED autolearn=disabled version=3.3.2 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 Received: from lepiller.eu ([2a00:5884:8208::1]:43042) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1ioFB7-0005Lb-1C; Sun, 05 Jan 2020 18:19:25 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 8285a479; Sun, 5 Jan 2020 23:19:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=lepiller.eu; h=date :in-reply-to:references:mime-version:content-type :content-transfer-encoding:subject:to:cc:from:message-id; s= dkim; bh=gfP+0x3E0pfpcyAsJIDMuY1VaSA=; b=d8jnJa6acVckD0OOyaFud/T sRw/kFmKDwr1YH87iZzYhHGGVOCfDXfLG25S5X9zFR5B5ccaiHhsxTxrueVqMHEt wbBtF6CM9AgWgwXrSp5o5vJXbz0eeOsP7vJSE/keMEXFy0OKRrbQCqnrKJRqNG4F pLK2VA0uk9JYOEmVraxElj9TVV8Ea0eLPCpWG62w/eICe2wqihGDib0rft/C84iH pzRwFRu5ihzlC9CeaFMjs8reYV4vYibVRqhuA/4KKb4ijJ4yhAArv5nSL/w8aSFb GYr7jiaBGRpWP3jc+TMBNn2kczM8jOXbKj6cyLrNL9D31rmGi6HyrRt7VBnvroA= = Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 94038e0c (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Sun, 5 Jan 2020 23:19:18 +0000 (UTC) Date: Sun, 05 Jan 2020 18:19:10 -0500 User-Agent: K-9 Mail for Android In-Reply-To: <87imlpy07j.fsf@gnu.org> References: <87imlpy07j.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums To: Brett Gilio ,bug-guix@gnu.org From: Julien Lepiller Message-ID: <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:5884:8208::1 X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: submit Cc: bandali@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) 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 From debbugs-submit-bounces@debbugs.gnu.org Sun Jan 05 22:17:14 2020 Received: (at 38959) by debbugs.gnu.org; 6 Jan 2020 03:17:14 +0000 Received: from localhost ([127.0.0.1]:44881 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioItF-00033J-Pg for submit@debbugs.gnu.org; Sun, 05 Jan 2020 22:17:14 -0500 Received: from eggs.gnu.org ([209.51.188.92]:43956) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioItE-00032y-16 for 38959@debbugs.gnu.org; Sun, 05 Jan 2020 22:17:12 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:47716) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioIt8-0002iA-9z; Sun, 05 Jan 2020 22:17:06 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=46978 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioIt7-0002B6-BO; Sun, 05 Jan 2020 22:17:05 -0500 From: Brett Gilio To: Julien Lepiller Subject: Re: bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums References: <87imlpy07j.fsf@gnu.org> <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> Date: Sun, 05 Jan 2020 21:17:10 -0600 In-Reply-To: <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> (Julien Lepiller's message of "Sun, 05 Jan 2020 18:19:10 -0500") Message-ID: <877e25xoi1.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38959 Cc: bandali@gnu.org, 38959@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) 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] From debbugs-submit-bounces@debbugs.gnu.org Mon Jan 06 03:39:45 2020 Received: (at 38959-done) by debbugs.gnu.org; 6 Jan 2020 08:39:46 +0000 Received: from localhost ([127.0.0.1]:44991 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNvN-0003Ls-NG for submit@debbugs.gnu.org; Mon, 06 Jan 2020 03:39:45 -0500 Received: from eggs.gnu.org ([209.51.188.92]:35985) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ioNvL-0003Ld-AP for 38959-done@debbugs.gnu.org; Mon, 06 Jan 2020 03:39:43 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:50996) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ioNvF-0007Ee-Gt; Mon, 06 Jan 2020 03:39:37 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48346 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ioNvE-0000HK-BR; Mon, 06 Jan 2020 03:39:36 -0500 From: Brett Gilio To: Julien Lepiller Subject: Re: bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums References: <87imlpy07j.fsf@gnu.org> <5CD843B3-688A-4BBB-A5E3-1A9CF45A7E00@lepiller.eu> <877e25xoi1.fsf@gnu.org> Date: Mon, 06 Jan 2020 02:39:44 -0600 In-Reply-To: <877e25xoi1.fsf@gnu.org> (Brett Gilio's message of "Sun, 05 Jan 2020 21:17:10 -0600") Message-ID: <8736ctvuzz.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38959-done Cc: 38959-done@debbugs.gnu.org, bandali@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) 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] From unknown Sat Aug 09 13:07:06 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Mon, 03 Feb 2020 12:24:06 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator