GNU bug report logs -
#38959
Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums
Previous Next
Reported by: Brett Gilio <brettg <at> gnu.org>
Date: Sun, 5 Jan 2020 23:05:02 UTC
Severity: normal
Done: Brett Gilio <brettg <at> gnu.org>
Bug is archived. No further changes may be made.
Full log
Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):
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.
--
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg <at> gnu.org> <brettg <at> posteo.net>
This bug report was last modified 5 years and 190 days ago.
Previous Next
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.