[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Bug? coqide missing? (in package coq, version 8.11.2)

From: Julien Lepiller
Subject: Re: Bug? coqide missing? (in package coq, version 8.11.2)
Date: Sat, 20 Mar 2021 22:04:28 -0400
User-agent: K-9 Mail for Android

Le 20 mars 2021 20:34:48 GMT-04:00, zimoun <> a écrit :
>Hi Julien
>On Sat, 20 Mar 2021 at 19:53, Julien Lepiller <>
>> guix size coq -> 869.7 MB
>> guix size coq:ide -> 1557.0 MB
>Yeah, but you have a high probability to have already have these

We originally built coqide with coq itself. Because of the huge closure size, 
we decided to split the package in two. In this condition, the split is a win. 
Also, why couldn't I build a coq package on a headless server? I don't want 
graphics in that case :)

>> Almost twice as much, because this brings in graphical
>> dependencies. Separating packages to multiple outputs can reduce the
>> closure size of some outputs, but if you build the package, you get
>> the same number of dependencies as if there were a single output. You
>> have everything to gain if you get substitutes, and nothing to lose
>> you don't have any or want to use the more expensive output. 
>You loose what I wrote: more dependencies and less discoverability. :-)

Why more dependencies? There are either the same amount if you want coq:ide, or 
less than before if you don't.

>I agree it reduces the closure size.  But it is not different to have
>different packages using inherit, right.
>Well, it seems a matter of taste. :-)

And a matter of what's supported upstream. I don't think coq sources let you 
build coqide alone very easily.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]