GNU bug report logs - #33745
Unnecessary dependencies in Coq

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 33745 in the body.
You can then email your comments to 33745 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: bug-guix <at> gnu.org
Subject: Unnecessary dependencies in Coq
Date: Fri, 14 Dec 2018 15:59:17 +0100

I believe that the current Coq package [1] pulls in way too many dependencies.

Firstly, as it was already mentioned on Guix-devel [2], the package pulls in texlive and Hevea.
I think those are needed only for building the pdf reference manual.

Secondly, the Coq package depends on lablgtk -- I guess this is needed for building CoqIDE.
Unfortunately, it seems that due to this dependency, the package pulls in all sorts of stuff, including gstreamer and jack!
The dependency graph generated by `guix graph coq` is absolutely huge.

I think it would be beneficial to split the CoqIDE into a separate package for this reason.


[1]: https://git.savannah.gnu.org/cgit/guix.git/tree/gnu/packages/ocaml.scm#n628
[2]: https://lists.gnu.org/archive/html/guix-devel/2018-12/msg00291.html

Message #8 received at 33745 <at> debbugs.gnu.org (full text, mbox):

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: 33745 <at> debbugs.gnu.org
Subject: Re: Unnecessary dependencies in Coq
Date: Fri, 14 Dec 2018 17:45:00 +0100

Oh, I forgot about another potential issue: right now the Coq package _hardcodes_ the use of Icecat as a default browser:


       (modify-phases %standard-phases
         (replace 'configure
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (mandir (string-append out "/share/man"))
                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
               (invoke "./configure"
                       "-prefix" out
                       "-mandir" mandir
                       "-browser" browser
                       "-coqide" "opt")))) ..


Can this be avoided somehow?

Message #11 received at 33745 <at> debbugs.gnu.org (full text, mbox):

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: 33745 <at> debbugs.gnu.org
Date: Tue, 18 Dec 2018 12:38:02 +0100

Well it looks like this has been resolved in 8a2cfc7bea37fd5cc5d384ac16d7cd3bd5603ab9

Message #14 received at 33745 <at> debbugs.gnu.org (full text, mbox):

From: Gábor Boskovits <boskovits <at> gmail.com>
To: Dan Frumin <dfrumin <at> cs.ru.nl>
Cc: 33745 <at> debbugs.gnu.org
Subject: Re: bug#33745: Unnecessary dependencies in Coq
Date: Tue, 18 Dec 2018 16:20:18 +0100

Hello Dan,

It would be nice to include the bug title in the subject, so people
looking at the mail don't have to go to the issue tracker to see what
the mail refers to.

Dan Frumin <dfrumin <at> cs.ru.nl> ezt írta (időpont: 2018. dec. 18., K, 15:54):
>
> Well it looks like this has been resolved in 8a2cfc7bea37fd5cc5d384ac16d7cd3bd5603ab9
>
>
>

I have seen two other problems raised on this issue. If they are still
relevant, please retitle this issue to reflect the new state.
You can do that by sending a mail to the control server. You can have
a look at the control commands at
https://debbugs.gnu.org/server-control.html.

If you feel this issue can be closed, please feel free to do so by
sending a message to 33745-done <at> debbugs.gnu.org.

Best regards,
g_bor

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.