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

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

[yasu]

Hello,

After installing COQ using:
   guix install coq

I was perplexed that I could not find the coqide program.
Howerver, GUIX does seem to build it:


~$ guix build coq
   /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-ide
   /gnu/store/n8g37cv0028wds959rjgpl5dsj3p3xl0-coq-8.11.2

~$ ls /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-ide/bin
   coqide


The fact that this coqide is not brought to user profile - is this a
bug? 😅

-Yasu

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

[Julien Lepiller]

Hi Yasu,

This is not a bug: coqide brings a lot of dependencies, so it's in a separate output, as you can see with guix search or guix show. To install it, install the ide output, like so:

guix install coq:ide

Le 20 mars 2021 02:11:30 GMT-04:00, yasu <yasu@yasuaki.com> a écrit :
>
>Hello,
>
>After installing COQ using:
>   guix install coq
>
>I was perplexed that I could not find the coqide program.
>Howerver, GUIX does seem to build it:
>
>
>~$ guix build coq
>   /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-ide
>   /gnu/store/n8g37cv0028wds959rjgpl5dsj3p3xl0-coq-8.11.2
>
>~$ ls /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-ide/bin
>   coqide
>
>
>The fact that this coqide is not brought to user profile - is this a
>bug? 😅
>
>-Yasu

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

[yasu]

Hi Julien,

Ohhhh, I see, I didn't know anything about these "sub-packages" that
follow colon.

Is there anything we can do to make it less confusing?

One way would be to allow the user to type coqide, or whatever the
executable they please, and search for all the possible package names
and suggest a way to install an existing package that matches.

I imagine something like:

> coqide

* The command coqide is provided by coq:ide.  To install it, run:

    guix install coq:ide

> 

:-)
Yasu




On Sat, 2021-03-20 at 06:48 -0400, Julien Lepiller wrote:
> Hi Yasu,
> 
> This is not a bug: coqide brings a lot of dependencies, so it's in a
> separate output, as you can see with guix search or guix show. To
> install it, install the ide output, like so:
> 
> guix install coq:ide
> 
> Le 20 mars 2021 02:11:30 GMT-04:00, yasu <yasu@yasuaki.com> a écrit :
> > Hello,
> > 
> > After installing COQ using:
> >    guix install coq
> > 
> > I was perplexed that I could not find the coqide program.
> > Howerver, GUIX does seem to build it:
> > 
> > 
> > ~$ guix build coq
> >    /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-ide
> >    /gnu/store/n8g37cv0028wds959rjgpl5dsj3p3xl0-coq-8.11.2
> > 
> > ~$ ls /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-
> > ide/bin
> >    coqide
> > 
> > 
> > The fact that this coqide is not brought to user profile - is this
> > a
> > bug? 😅
> > 
> > -Yasu
> > 
> > 

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

[zimoun]

Hi Julien,

On Sat, 20 Mar 2021 at 06:48, Julien Lepiller <julien@lepiller.eu> wrote:

> This is not a bug: coqide brings a lot of dependencies, so it's in a

What do you mean?

--8<---------------cut here---------------start------------->8---
$ guix package -i coq -n
The following package would be installed:
   coq 8.11.2

125.8 MB would be downloaded

$ guix package -i coq:ide -n
The following package would be installed:
   coq:ide 8.11.2

125.8 MB would be downloaded

$ guix package -i coq coq:ide -n
The following packages would be installed:
   coq     8.11.2
   coq:ide 8.11.2

125.8 MB would be downloaded
--8<---------------cut here---------------end--------------->8---


> separate output, as you can see with guix search or guix show. To
> install it, install the ide output, like so: 
>
> guix install coq:ide

I am always confused by these multi-outputs packages, as git:send-email
or coq:ide or th recent “ocaml-z3“.  They often increase the number of
build-time dependencies and they are less discoverable, IMHO.

They make sense for -doc or -debug but otherwise they appear to me
confusing.


Cheers,
simon

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

[Julien Lepiller]

guix size coq -> 869.7 MB
guix size coq:ide -> 1557.0 MB

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.

Le 20 mars 2021 12:39:20 GMT-04:00, zimoun <zimon.toutoune@gmail.com> a écrit :
>Hi Julien,
>
>On Sat, 20 Mar 2021 at 06:48, Julien Lepiller <julien@lepiller.eu>
>wrote:
>
>> This is not a bug: coqide brings a lot of dependencies, so it's in a
>
>What do you mean?
>
>--8<---------------cut here---------------start------------->8---
>$ guix package -i coq -n
>The following package would be installed:
>   coq 8.11.2
>
>125.8 MB would be downloaded
>
>$ guix package -i coq:ide -n
>The following package would be installed:
>   coq:ide 8.11.2
>
>125.8 MB would be downloaded
>
>$ guix package -i coq coq:ide -n
>The following packages would be installed:
>   coq     8.11.2
>   coq:ide 8.11.2
>
>125.8 MB would be downloaded
>--8<---------------cut here---------------end--------------->8---
>
>
>> separate output, as you can see with guix search or guix show. To
>> install it, install the ide output, like so: 
>>
>> guix install coq:ide
>
>I am always confused by these multi-outputs packages, as git:send-email
>or coq:ide or th recent “ocaml-z3“.  They often increase the number of
>build-time dependencies and they are less discoverable, IMHO.
>
>They make sense for -doc or -debug but otherwise they appear to me
>confusing.
>
>
>Cheers,
>simon

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

[zimoun]

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.


> 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. :-)

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. :-)

Cheers,
simon

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

[Julien Lepiller]

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

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

[zimoun]

Hi Julien,

On Sat, 20 Mar 2021 at 22:04, Julien Lepiller <julien@lepiller.eu> wrote:
> Le 20 mars 2021 20:34:48 GMT-04:00, zimoun <zimon.toutoune@gmail.com>
> a écrit

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

*more dependencies when you build it.  I agree that when the substitute
 is available, mutlioutput saves resources.


Cheers,
simon