Unnecessary dependencies in Coq

  • Done
  • quality assurance status badge
Details
3 participants
  • Gábor Boskovits
  • Dan Frumin
  • Ludovic Courtès
Owner
unassigned
Submitted by
Dan Frumin
Severity
normal
D
D
Dan Frumin wrote on 14 Dec 2018 15:59
(address . bug-guix@gnu.org)
83ee8918-ced3-310e-8cbf-9bd08d9036c5@cs.ru.nl
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.


D
D
Dan Frumin wrote on 14 Dec 2018 17:45
(address . 33745@debbugs.gnu.org)
86e609d6-86ce-3b3b-d8ff-3e87c33c339a@cs.ru.nl
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?
D
D
Dan Frumin wrote on 18 Dec 2018 12:38
(no subject)
(address . 33745@debbugs.gnu.org)
9c1d66c2-dda1-af87-b648-29a00d3dbc2d@cs.ru.nl
Well it looks like this has been resolved in 8a2cfc7bea37fd5cc5d384ac16d7cd3bd5603ab9
G
G
Gábor Boskovits wrote on 18 Dec 2018 16:20
Re: bug#33745: Unnecessary dependencies in Coq
(name . Dan Frumin)(address . dfrumin@cs.ru.nl)(address . 33745@debbugs.gnu.org)
CAE4v=pjpmfGch8F-mnZYV+MxWg8+J7cw_-UpQBsQQn9=YKzONA@mail.gmail.com
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@cs.ru.nl> ezt írta (id?pont: 2018. dec. 18., K, 15:54):
Toggle quote (6 lines)
>
> 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

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

Best regards,
g_bor
L
L
Ludovic Courtès wrote on 16 Jan 2019 12:00
control message for bug #33745
(address . control@debbugs.gnu.org)
87sgxsvpcl.fsf@gnu.org
tags 33745 fixed
close 33745
?
Your comment

This issue is archived.

To comment on this conversation send an email to 33745@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 33745
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch