From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id ng0PKNKpVmCeTQAA0tVLHw (envelope-from ) for ; Sun, 21 Mar 2021 02:05:06 +0000 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id GABRI9KpVmB+RQAAB5/wlQ (envelope-from ) for ; Sun, 21 Mar 2021 02:05:06 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id D3ECE21965 for ; Sun, 21 Mar 2021 03:05:05 +0100 (CET) Received: from localhost ([::1]:34650 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lNnSh-0001kj-Ka for larch@yhetil.org; Sat, 20 Mar 2021 22:05:03 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:39746) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lNnSQ-0001kb-RQ for help-guix@gnu.org; Sat, 20 Mar 2021 22:04:47 -0400 Received: from lepiller.eu ([2a00:5884:8208::1]:34720) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lNnSO-0000uE-Rh for help-guix@gnu.org; Sat, 20 Mar 2021 22:04:46 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 8df96231; Sun, 21 Mar 2021 02:04:39 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date :in-reply-to:references:mime-version:content-type :content-transfer-encoding:subject:to:from:message-id; s=dkim; bh=9AY+PLN1rIxvH9DTu8RSKvxRW6XSKIEOTXD/t8JUb0Y=; b=XwayWvTdsAYx gJsvpa70/Bq3xixtLdh9N+vp9EK2YyerfyFbWIyUwsT26kOoXy+YTKhuv5XE6WzA LzcQxTRErnK/Uec8KYwod8TaF/yi46Sas0P4pvvFCL57+7W2wdJmEYOgPjS3TtPM 4SqA+j4Kwek3SSgC9e0J63dYVLcYI5uQ8m8XdvBz0n8fLNugoeP0F8IEUihLalY2 UgCoPABDiC4RifITfk7xBexV0DaVYNpW9zerSalY7R+LIhMFsgOx5JwLwwOWPo9H z0n3l2n0EufYwSe7NZ/sttcrfIW97aRLsiG63Bfp6OimqtUlVKmSYdK1xfx7vTr+ AwtUDul7IA== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id f4078a05 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Sun, 21 Mar 2021 02:04:38 +0000 (UTC) Date: Sat, 20 Mar 2021 22:04:28 -0400 User-Agent: K-9 Mail for Android In-Reply-To: <86pmztuyxj.fsf@gmail.com> References: <751596538845b1dc9ec134d0148301f964b44246.camel@yasuaki.com> <08B18747-D14D-4D0E-91ED-A7E06BCFAA77@lepiller.eu> <86k0q1wzif.fsf@gmail.com> <6A74F875-3E74-444B-94DD-ECDB4BAF1069@lepiller.eu> <86pmztuyxj.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: Bug? coqide missing? (in package coq, version 8.11.2) To: zimoun ,help-guix@gnu.org From: Julien Lepiller Message-ID: <538339B4-60BA-4E5E-8BA0-A21B64EFB608@lepiller.eu> Received-SPF: pass client-ip=2a00:5884:8208::1; envelope-from=julien@lepiller.eu; helo=lepiller.eu X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: help-guix@gnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-guix-bounces+larch=yhetil.org@gnu.org Sender: "Help-Guix" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1616292306; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=Xa95mi6cIzU0YVZCFnWlK9XF7aVx/o30ruO5wMNfwDQ=; b=liZSSKircIfhvjBLi0+NcWt57qza+PIMASnNxi1HKB8ip6jvhdSTErNFyso7/vdpfX0P3S qsn4VMCP37cIemMVD9qEzVOpTgdok/duFtibLKpa9U4R47jDqgNJTpXWUiSnUiCnGucq9y e7tB/BNbAD5ipaWaA+8xqQv5ZM7cAYFqR7WlaCR86g+2WNjypsmD3AHOmsLNAJTKZNUQAY 93C9EvO7d8ZSYLjk4v/kTn+bYMqEXMYEyR975V8pvl9qAkm0H9CHhdOIJv7lmUinn/N0mO JVB9HHeXhaeKaWf39vWTEuujVGdqIGV8HRJBn+XAVkb23hRY6cIwhXwjq/j/SA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1616292306; a=rsa-sha256; cv=none; b=imcK5tLh/T6Io/o13xXvAJ6KvlivXu6kbYqC2qA7l3Ar1UBfZ4Emzm4Q+kANhVn0gsbQcK dwv5J/We4Phyz0d0I6s1pxAJgpgKKBayA6UywC/5LSEc3NHEIU7IGEJeEkqg/jstTg9eB4 SvtVR/g97ppFaW4HxBVW0D38H+XA1rlOsRGdk2B9aTYlhMFkfOCS+Toavzq+Rn5MdnLJup dtGyWIYIjjWjSBUu9ra4/5KSVJXUuCN1hDffNSRj8asIwsy08Egq8cBE9PKXLioCR/FoNs RE+Ds17KNhZ6k+1JKURdbzD7QImfAe6e4s2XCGfnLzj0vFzmMNEhWDZyEUiO4g== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=lepiller.eu header.s=dkim header.b=XwayWvTd; dmarc=pass (policy=none) header.from=lepiller.eu; spf=pass (aspmx1.migadu.com: domain of help-guix-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=help-guix-bounces@gnu.org X-Migadu-Spam-Score: -3.11 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=lepiller.eu header.s=dkim header.b=XwayWvTd; dmarc=pass (policy=none) header.from=lepiller.eu; spf=pass (aspmx1.migadu.com: domain of help-guix-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=help-guix-bounces@gnu.org X-Migadu-Queue-Id: D3ECE21965 X-Spam-Score: -3.11 X-Migadu-Scanner: scn0.migadu.com X-TUID: zcwvhIVrav15 Le 20 mars 2021 20:34:48 GMT-04:00, zimoun = a =C3=A9crit : >Hi Julien > >On Sat, 20 Mar 2021 at 19:53, Julien Lepiller >wrote: >> guix size coq -> 869=2E7 MB >> guix size coq:ide -> 1557=2E0 MB > >Yeah, but you have a high probability to have already have these >dependencies=2E We originally built coqide with coq itself=2E Because of the huge closure = size, we decided to split the package in two=2E In this condition, the spli= t is a win=2E Also, why couldn't I build a coq package on a headless server= ? I don't want graphics in that case :) > > >> Almost twice as much, because this brings in graphical >> dependencies=2E Separating packages to multiple outputs can reduce the >> closure size of some outputs, but if you build the package, you get >> the same number of dependencies as if there were a single output=2E You >> have everything to gain if you get substitutes, and nothing to lose >if >> you don't have any or want to use the more expensive output=2E=20 > >You loose what I wrote: more dependencies and less discoverability=2E :-) Why more dependencies? There are either the same amount if you want coq:id= e, or less than before if you don't=2E > >I agree it reduces the closure size=2E But it is not different to have >different packages using inherit, right=2E > >Well, it seems a matter of taste=2E :-) And a matter of what's supported upstream=2E I don't think coq sources let= you build coqide alone very easily=2E > >Cheers, >simon