From mboxrd@z Thu Jan 1 00:00:00 1970 From: Dan Frumin Subject: bug#33745: Unnecessary dependencies in Coq Date: Fri, 14 Dec 2018 15:59:17 +0100 Message-ID: <83ee8918-ced3-310e-8cbf-9bd08d9036c5@cs.ru.nl> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:49034) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gXqJr-00080f-LB for bug-guix@gnu.org; Fri, 14 Dec 2018 11:28:09 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gXqJm-0002bs-Py for bug-guix@gnu.org; Fri, 14 Dec 2018 11:28:06 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:44227) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gXqJm-0002bl-Lh for bug-guix@gnu.org; Fri, 14 Dec 2018 11:28:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gXqJm-0003Ab-DY for bug-guix@gnu.org; Fri, 14 Dec 2018 11:28:02 -0500 Sender: "Debbugs-submit" Resent-Message-ID: Received: from eggs.gnu.org ([2001:4830:134:3::10]:44674) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gXow5-0000Bv-K7 for bug-guix@gnu.org; Fri, 14 Dec 2018 09:59:30 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gXovx-0003wG-D3 for bug-guix@gnu.org; Fri, 14 Dec 2018 09:59:27 -0500 Received: from smtp1.science.ru.nl ([131.174.16.143]:46332) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gXovw-0003uR-VT for bug-guix@gnu.org; Fri, 14 Dec 2018 09:59:21 -0500 Received: from [192.168.2.8] (ip565a9ee0.direct-adsl.nl [86.90.158.224] (may be forged)) (authen=dfrumin) by smtp1.science.ru.nl (8.14.4/5.32) with ESMTP id wBEExHsG012446 for ; Fri, 14 Dec 2018 15:59:17 +0100 Content-Language: en-US List-Id: Bug reports for GNU Guix List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-guix-bounces+gcggb-bug-guix=m.gmane.org@gnu.org Sender: "bug-Guix" To: 33745@debbugs.gnu.org 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