GNU bug report logs - #33745
Unnecessary dependencies in Coq

Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.

Package: guix; Reported by: Dan Frumin <dfrumin@HIDDEN>; Keywords: fixed; Done: Ludovic Courtès <ludo@HIDDEN>; Maintainer for guix is bug-guix@HIDDEN.
bug closed, send any further explanations to 33745 <at> debbugs.gnu.org and Dan Frumin <dfrumin@HIDDEN> Request was from Ludovic Courtès <ludo@HIDDEN> to control <at> debbugs.gnu.org. Full text available.
Added tag(s) fixed. Request was from Ludovic Courtès <ludo@HIDDEN> to control <at> debbugs.gnu.org. Full text available.

Message received at 33745 <at> debbugs.gnu.org:


Received: (at 33745) by debbugs.gnu.org; 18 Dec 2018 15:20:39 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Dec 18 10:20:39 2018
Received: from localhost ([127.0.0.1]:53568 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1gZHAk-0005cA-Mk
	for submit <at> debbugs.gnu.org; Tue, 18 Dec 2018 10:20:38 -0500
Received: from mail-it1-f182.google.com ([209.85.166.182]:40855)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <boskovits@HIDDEN>) id 1gZHAh-0005bv-4m
 for 33745 <at> debbugs.gnu.org; Tue, 18 Dec 2018 10:20:35 -0500
Received: by mail-it1-f182.google.com with SMTP id h193so4690801ita.5
 for <33745 <at> debbugs.gnu.org>; Tue, 18 Dec 2018 07:20:35 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
 h=mime-version:references:in-reply-to:from:date:message-id:subject:to
 :cc:content-transfer-encoding;
 bh=EAkYJ/SQQfTpcDh3ThxNSnHyAzkSjSgxa3Ce+PxMXZg=;
 b=Fe3x29seBsfttKoypN/PEtJWm+49lmOLumS4/ItqkkPUTAtIZkoMLJqoNjR3neCyiY
 s5AVTOqHRp8QybWGTz6ZAD1gkYuVBdu9gY0s/epuHkRWnIOghDY2z8dtQsaavP2EoJGf
 K9y4GmIqadVqyrJe9VtZEHs2dNvvqJa7TC3ZGVOpmhcj3ATUNWXSzeKd6HMbUVHHl8QI
 526pb9gUNUZyNK6MUQlxOkxTfZmn4OAvPrOssz1htrxL6QdtU73/xAa1xDtOUBDoztpO
 Baj5rZWrCMmLIWVH3XPRAfvLL9WlhjTvbGdVJ4S1m98DYKvVhnPkP2IpPYBQAIIKCHPV
 2EbA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20161025;
 h=x-gm-message-state:mime-version:references:in-reply-to:from:date
 :message-id:subject:to:cc:content-transfer-encoding;
 bh=EAkYJ/SQQfTpcDh3ThxNSnHyAzkSjSgxa3Ce+PxMXZg=;
 b=AyjSlbjnnMuLFs5tJzNCN0ve5MocKEn3FmCuy6V3XqwRNNlc/lCnTfSX6jiTb1Z9ln
 tjR9DOMHxvN+Qt0xTGb4jLKxWsrUexKXc7UHzkXhyga/GEcR0Y0pygySFp3X+uOtmhF/
 Lz85cF31UYNZq1tW1icJNF/UGgek8TgWa1QmHHmMO/2aqDDBbEw+UtgGmMNPVWHGgvDE
 wup+91oMGePd0Oi1scbcgpvud1jogLWh+4OC1TBEkUIRDoJmWWw8eA7oJaUPyCFUvdN9
 yGh1GUbwzHDDOzApctZigJMnN2WZ34CZT/qx7LaTHn0vmmhP4IoDFsYJOzQa8Jjup6r5
 gyww==
X-Gm-Message-State: AA+aEWbKGjc8uEyqDz8Awbt3wu5YFBzQNPcjVcmi+pW6kmQ1ocQOgSHT
 zDn9JmE9GFyW1nTFYL3bgknn3gHPaNIeuKGSag==
X-Google-Smtp-Source: AFSGD/X+v2wBYSytAyveri4X96Feix9dpZclKT7D4fvTJShv1ZkqPlwNvBa8SXUjpYLEomuOig7Iw4nCTTJpWvYATjQ=
X-Received: by 2002:a05:660c:a8f:: with SMTP id
 m15mr3221195itk.114.1545146429490; 
 Tue, 18 Dec 2018 07:20:29 -0800 (PST)
MIME-Version: 1.0
References: <83ee8918-ced3-310e-8cbf-9bd08d9036c5@HIDDEN>
 <9c1d66c2-dda1-af87-b648-29a00d3dbc2d@HIDDEN>
In-Reply-To: <9c1d66c2-dda1-af87-b648-29a00d3dbc2d@HIDDEN>
From: =?UTF-8?Q?G=C3=A1bor_Boskovits?= <boskovits@HIDDEN>
Date: Tue, 18 Dec 2018 16:20:18 +0100
Message-ID: <CAE4v=pjpmfGch8F-mnZYV+MxWg8+J7cw_-UpQBsQQn9=YKzONA@HIDDEN>
Subject: Re: bug#33745: Unnecessary dependencies in Coq
To: Dan Frumin <dfrumin@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 33745
Cc: 33745 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

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@HIDDEN> ezt =C3=ADrta (id=C5=91pont: 2018. dec. 18., =
K, 15:54):
>
> Well it looks like this has been resolved in 8a2cfc7bea37fd5cc5d384ac16d7=
cd3bd5603ab9
>
>
>

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




Information forwarded to bug-guix@HIDDEN:
bug#33745; Package guix. Full text available.

Message received at 33745 <at> debbugs.gnu.org:


Received: (at 33745) by debbugs.gnu.org; 18 Dec 2018 11:38:09 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Dec 18 06:38:09 2018
Received: from localhost ([127.0.0.1]:52709 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1gZDhR-0006UX-5S
	for submit <at> debbugs.gnu.org; Tue, 18 Dec 2018 06:38:09 -0500
Received: from smtp1.science.ru.nl ([131.174.16.143]:37088)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <dfrumin@HIDDEN>) id 1gZDhP-0006UL-Cx
 for 33745 <at> debbugs.gnu.org; Tue, 18 Dec 2018 06:38:08 -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 wBIBc2cG030356
 for <33745 <at> debbugs.gnu.org>; Tue, 18 Dec 2018 12:38:02 +0100
To: 33745 <at> debbugs.gnu.org
From: Dan Frumin <dfrumin@HIDDEN>
Message-ID: <9c1d66c2-dda1-af87-b648-29a00d3dbc2d@HIDDEN>
Date: Tue, 18 Dec 2018 12:38:02 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101
 Thunderbird/60.2.1
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
X-Spam-Score: -0.3 (/)
X-Debbugs-Envelope-To: 33745
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.3 (-)

Well it looks like this has been resolved in 8a2cfc7bea37fd5cc5d384ac16d7cd3bd5603ab9




Information forwarded to bug-guix@HIDDEN:
bug#33745; Package guix. Full text available.

Message received at 33745 <at> debbugs.gnu.org:


Received: (at 33745) by debbugs.gnu.org; 14 Dec 2018 16:45:04 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Dec 14 11:45:04 2018
Received: from localhost ([127.0.0.1]:48491 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1gXqaG-0003b4-9a
	for submit <at> debbugs.gnu.org; Fri, 14 Dec 2018 11:45:04 -0500
Received: from smtp2.science.ru.nl ([131.174.16.145]:50922)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <dfrumin@HIDDEN>) id 1gXqaE-0003ar-Ti
 for 33745 <at> debbugs.gnu.org; Fri, 14 Dec 2018 11:45:03 -0500
Received: from [192.168.2.8] (ip565a9ee0.direct-adsl.nl [86.90.158.224] (may
 be forged)) (authen=dfrumin)
 by smtp2.science.ru.nl (8.14.4/5.32) with ESMTP id wBEGj0Rp009147
 for <33745 <at> debbugs.gnu.org>; Fri, 14 Dec 2018 17:45:01 +0100
From: Dan Frumin <dfrumin@HIDDEN>
To: 33745 <at> debbugs.gnu.org
Subject: Re: Unnecessary dependencies in Coq
Message-ID: <86e609d6-86ce-3b3b-d8ff-3e87c33c339a@HIDDEN>
Date: Fri, 14 Dec 2018 17:45:00 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101
 Thunderbird/60.2.1
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
X-Spam-Score: -2.3 (--)
X-Debbugs-Envelope-To: 33745
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -3.3 (---)

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?




Information forwarded to bug-guix@HIDDEN:
bug#33745; Package guix. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 14 Dec 2018 16:27:38 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Dec 14 11:27:38 2018
Received: from localhost ([127.0.0.1]:48485 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1gXqJN-00039l-Bq
	for submit <at> debbugs.gnu.org; Fri, 14 Dec 2018 11:27:37 -0500
Received: from eggs.gnu.org ([208.118.235.92]:35119)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <dfrumin@HIDDEN>) id 1gXowK-0000wp-Ko
 for submit <at> debbugs.gnu.org; Fri, 14 Dec 2018 09:59:45 -0500
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
 (envelope-from <dfrumin@HIDDEN>) id 1gXow9-00042Z-Ec
 for submit <at> debbugs.gnu.org; Fri, 14 Dec 2018 09:59:39 -0500
X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=disabled
 version=3.3.2
Received: from lists.gnu.org ([2001:4830:134:3::11]:58262)
 by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32)
 (Exim 4.71) (envelope-from <dfrumin@HIDDEN>) id 1gXow6-00041o-Qn
 for submit <at> debbugs.gnu.org; Fri, 14 Dec 2018 09:59:31 -0500
Received: from eggs.gnu.org ([2001:4830:134:3::10]:44674)
 by lists.gnu.org with esmtp (Exim 4.71)
 (envelope-from <dfrumin@HIDDEN>) id 1gXow5-0000Bv-K7
 for bug-guix@HIDDEN; Fri, 14 Dec 2018 09:59:30 -0500
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
 (envelope-from <dfrumin@HIDDEN>) id 1gXovx-0003wG-D3
 for bug-guix@HIDDEN; 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 <dfrumin@HIDDEN>) id 1gXovw-0003uR-VT
 for bug-guix@HIDDEN; 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 <bug-guix@HIDDEN>; Fri, 14 Dec 2018 15:59:17 +0100
To: bug-guix@HIDDEN
From: Dan Frumin <dfrumin@HIDDEN>
Subject: Unnecessary dependencies in Coq
Message-ID: <83ee8918-ced3-310e-8cbf-9bd08d9036c5@HIDDEN>
Date: Fri, 14 Dec 2018 15:59:17 +0100
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101
 Thunderbird/60.2.1
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic]
 [fuzzy]
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x
X-Received-From: 2001:4830:134:3::11
X-Spam-Score: -4.0 (----)
X-Debbugs-Envelope-To: submit
X-Mailman-Approved-At: Fri, 14 Dec 2018 11:27:36 -0500
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -5.0 (-----)

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




Acknowledgement sent to Dan Frumin <dfrumin@HIDDEN>:
New bug report received and forwarded. Copy sent to bug-guix@HIDDEN. Full text available.
Report forwarded to bug-guix@HIDDEN:
bug#33745; Package guix. Full text available.
Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Last modified: Wed, 16 Jan 2019 11:15:01 UTC

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