* bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums
@ 2020-01-05 23:04 Brett Gilio
2020-01-05 23:19 ` Julien Lepiller
0 siblings, 1 reply; 4+ messages in thread
From: Brett Gilio @ 2020-01-05 23:04 UTC (permalink / raw)
To: 38959; +Cc: bandali
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@gnu.org> <brettg@posteo.net>
^ permalink raw reply [flat|nested] 4+ messages in thread
* bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums
2020-01-05 23:04 bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums Brett Gilio
@ 2020-01-05 23:19 ` Julien Lepiller
2020-01-06 3:17 ` Brett Gilio
0 siblings, 1 reply; 4+ messages in thread
From: Julien Lepiller @ 2020-01-05 23:19 UTC (permalink / raw)
To: brettg, 38959; +Cc: bandali
Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio <brettg@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.
^ permalink raw reply [flat|nested] 4+ messages in thread
* bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums
2020-01-05 23:19 ` Julien Lepiller
@ 2020-01-06 3:17 ` Brett Gilio
2020-01-06 8:39 ` Brett Gilio
0 siblings, 1 reply; 4+ messages in thread
From: Brett Gilio @ 2020-01-06 3:17 UTC (permalink / raw)
To: Julien Lepiller; +Cc: bandali, 38959
Julien Lepiller <julien@lepiller.eu> writes:
> Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio <brettg@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. :)
--
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>
^ permalink raw reply [flat|nested] 4+ messages in thread
* bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums
2020-01-06 3:17 ` Brett Gilio
@ 2020-01-06 8:39 ` Brett Gilio
0 siblings, 0 replies; 4+ messages in thread
From: Brett Gilio @ 2020-01-06 8:39 UTC (permalink / raw)
To: Julien Lepiller; +Cc: 38959-done, bandali
Brett Gilio <brettg@gnu.org> writes:
> Julien Lepiller <julien@lepiller.eu> writes:
>
>> Le 5 janvier 2020 18:04:16 GMT-05:00, Brett Gilio <brettg@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]
<brettg@gnu.org> <brettg@posteo.net>
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2020-01-06 8:40 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-01-05 23:04 bug#38959: Adding Coq 8.10.1 for Int63.Ring63 and Coq-Bignums Brett Gilio
2020-01-05 23:19 ` Julien Lepiller
2020-01-06 3:17 ` Brett Gilio
2020-01-06 8:39 ` Brett Gilio
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).