bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums

[Brett Gilio]

Brett Gilio <address@hidden> writes:

> Julien Lepiller <address@hidden> writes:
>
>> Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio <address@hidden> a écrit :
>>>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 case.
>>
>
> 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.

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<address@hidden> <address@hidden>