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

[Julien Lepiller]

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.