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

[Julien Lepiller <julien@lepiller.eu>]

Le 20 mars 2021 20:34:48 GMT-04:00, zimoun <zimon.toutoune@gmail.com> a écrit :
>Hi Julien
>
>On Sat, 20 Mar 2021 at 19:53, Julien Lepiller <julien@lepiller.eu>
>wrote:
>> 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
>dependencies.

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
>if
>> 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.

>
>Cheers,
>simon