unofficial mirror of help-guix@gnu.org 
 help / color / mirror / Atom feed
* Bug? coqide missing? (in package coq, version 8.11.2)
@ 2021-03-20  6:11 yasu
  2021-03-20 10:48 ` Julien Lepiller
  0 siblings, 1 reply; 8+ messages in thread
From: yasu @ 2021-03-20  6:11 UTC (permalink / raw)
  To: Help Guix


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



^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-20  6:11 Bug? coqide missing? (in package coq, version 8.11.2) yasu
@ 2021-03-20 10:48 ` Julien Lepiller
  2021-03-20 12:26   ` yasu
  2021-03-20 16:39   ` zimoun
  0 siblings, 2 replies; 8+ messages in thread
From: Julien Lepiller @ 2021-03-20 10:48 UTC (permalink / raw)
  To: help-guix, yasu

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

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-20 10:48 ` Julien Lepiller
@ 2021-03-20 12:26   ` yasu
  2021-03-20 16:39   ` zimoun
  1 sibling, 0 replies; 8+ messages in thread
From: yasu @ 2021-03-20 12:26 UTC (permalink / raw)
  To: Julien Lepiller, help-guix

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



^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-20 10:48 ` Julien Lepiller
  2021-03-20 12:26   ` yasu
@ 2021-03-20 16:39   ` zimoun
  2021-03-20 23:53     ` Julien Lepiller
  1 sibling, 1 reply; 8+ messages in thread
From: zimoun @ 2021-03-20 16:39 UTC (permalink / raw)
  To: Julien Lepiller, help-guix, yasu

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



^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-20 16:39   ` zimoun
@ 2021-03-20 23:53     ` Julien Lepiller
  2021-03-21  0:34       ` zimoun
  0 siblings, 1 reply; 8+ messages in thread
From: Julien Lepiller @ 2021-03-20 23:53 UTC (permalink / raw)
  To: zimoun, help-guix, yasu

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

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-20 23:53     ` Julien Lepiller
@ 2021-03-21  0:34       ` zimoun
  2021-03-21  2:04         ` Julien Lepiller
  0 siblings, 1 reply; 8+ messages in thread
From: zimoun @ 2021-03-21  0:34 UTC (permalink / raw)
  To: Julien Lepiller, help-guix, yasu

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


^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-21  0:34       ` zimoun
@ 2021-03-21  2:04         ` Julien Lepiller
  2021-03-21 12:06           ` zimoun
  0 siblings, 1 reply; 8+ messages in thread
From: Julien Lepiller @ 2021-03-21  2:04 UTC (permalink / raw)
  To: zimoun, help-guix



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


^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Bug? coqide missing? (in package coq, version 8.11.2)
  2021-03-21  2:04         ` Julien Lepiller
@ 2021-03-21 12:06           ` zimoun
  0 siblings, 0 replies; 8+ messages in thread
From: zimoun @ 2021-03-21 12:06 UTC (permalink / raw)
  To: Julien Lepiller, help-guix

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


^ permalink raw reply	[flat|nested] 8+ messages in thread

end of thread, other threads:[~2021-03-21 12:15 UTC | newest]

Thread overview: 8+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-03-20  6:11 Bug? coqide missing? (in package coq, version 8.11.2) yasu
2021-03-20 10:48 ` Julien Lepiller
2021-03-20 12:26   ` yasu
2021-03-20 16:39   ` zimoun
2021-03-20 23:53     ` Julien Lepiller
2021-03-21  0:34       ` zimoun
2021-03-21  2:04         ` Julien Lepiller
2021-03-21 12:06           ` zimoun

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