Brett Gilio <bre...@gnu.org> writes: > Julien Lepiller <jul...@lepiller.eu> writes: > >> Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio <bre...@gnu.org> 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] <bre...@gnu.org> <bre...@posteo.net>