Julien Lepiller <[email protected]> writes: > Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio <[email protected]> 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] <[email protected]> <[email protected]>
