From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 14 11:27:38 2018 Received: (at submit) by debbugs.gnu.org; 14 Dec 2018 16:27:38 +0000 Received: from localhost ([127.0.0.1]:48485 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gXqJN-00039l-Bq for submit@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 ) id 1gXowK-0000wp-Ko for submit@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 ) id 1gXow9-00042Z-Ec for submit@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 ) id 1gXow6-00041o-Qn for submit@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 ) 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 To: bug-guix@gnu.org From: Dan Frumin Subject: Unnecessary dependencies in Coq Message-ID: <83ee8918-ced3-310e-8cbf-9bd08d9036c5@cs.ru.nl> 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@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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 From debbugs-submit-bounces@debbugs.gnu.org Fri Dec 14 11:45:04 2018 Received: (at 33745) by debbugs.gnu.org; 14 Dec 2018 16:45:04 +0000 Received: from localhost ([127.0.0.1]:48491 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gXqaG-0003b4-9a for submit@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 ) id 1gXqaE-0003ar-Ti for 33745@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@debbugs.gnu.org>; Fri, 14 Dec 2018 17:45:01 +0100 From: Dan Frumin To: 33745@debbugs.gnu.org Subject: Re: Unnecessary dependencies in Coq Message-ID: <86e609d6-86ce-3b3b-d8ff-3e87c33c339a@cs.ru.nl> 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@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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? From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 18 06:38:09 2018 Received: (at 33745) by debbugs.gnu.org; 18 Dec 2018 11:38:09 +0000 Received: from localhost ([127.0.0.1]:52709 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZDhR-0006UX-5S for submit@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 ) id 1gZDhP-0006UL-Cx for 33745@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@debbugs.gnu.org>; Tue, 18 Dec 2018 12:38:02 +0100 To: 33745@debbugs.gnu.org From: Dan Frumin Message-ID: <9c1d66c2-dda1-af87-b648-29a00d3dbc2d@cs.ru.nl> 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@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.3 (-) Well it looks like this has been resolved in 8a2cfc7bea37fd5cc5d384ac16d7cd3bd5603ab9 From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 18 10:20:39 2018 Received: (at 33745) by debbugs.gnu.org; 18 Dec 2018 15:20:39 +0000 Received: from localhost ([127.0.0.1]:53568 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gZHAk-0005cA-Mk for submit@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 ) id 1gZHAh-0005bv-4m for 33745@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@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@cs.ru.nl> <9c1d66c2-dda1-af87-b648-29a00d3dbc2d@cs.ru.nl> In-Reply-To: <9c1d66c2-dda1-af87-b648-29a00d3dbc2d@cs.ru.nl> From: =?UTF-8?Q?G=C3=A1bor_Boskovits?= Date: Tue, 18 Dec 2018 16:20:18 +0100 Message-ID: Subject: Re: bug#33745: Unnecessary dependencies in Coq To: Dan Frumin Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 33745 Cc: 33745@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" 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 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@debbugs.gnu.org. Best regards, g_bor From debbugs-submit-bounces@debbugs.gnu.org Wed Jan 16 06:01:03 2019 Received: (at control) by debbugs.gnu.org; 16 Jan 2019 11:01:03 +0000 Received: from localhost ([127.0.0.1]:60773 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gjiwR-00028o-9c for submit@debbugs.gnu.org; Wed, 16 Jan 2019 06:01:03 -0500 Received: from hera.aquilenet.fr ([185.233.100.1]:46572) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gjiwP-000288-OO for control@debbugs.gnu.org; Wed, 16 Jan 2019 06:01:02 -0500 Received: from localhost (localhost [127.0.0.1]) by hera.aquilenet.fr (Postfix) with ESMTP id AF0391C4A for ; Wed, 16 Jan 2019 12:00:59 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at aquilenet.fr Received: from hera.aquilenet.fr ([127.0.0.1]) by localhost (hera.aquilenet.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id J1AibPDk31HI for ; Wed, 16 Jan 2019 12:00:59 +0100 (CET) Received: from ribbon (unknown [IPv6:2a01:e0a:1d:7270:af76:b9b:ca24:c465]) by hera.aquilenet.fr (Postfix) with ESMTPSA id D57A41C0A for ; Wed, 16 Jan 2019 12:00:58 +0100 (CET) Date: Wed, 16 Jan 2019 12:00:58 +0100 Message-Id: <87sgxsvpcl.fsf@gnu.org> To: control@debbugs.gnu.org From: =?utf-8?Q?Ludovic_Court=C3=A8s?= Subject: control message for bug #33745 MIME-version: 1.0 Content-type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: control X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) tags 33745 fixed close 33745 From unknown Sun Jun 22 11:46:57 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Wed, 13 Feb 2019 12:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator