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

[Brett Gilio]

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. :)

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