From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id cEChJiXqVWClAgAA0tVLHw (envelope-from ) for ; Sat, 20 Mar 2021 12:27:17 +0000 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0 with LMTPS id kGeBIiXqVWCpSwAA1q6Kng (envelope-from ) for ; Sat, 20 Mar 2021 12:27:17 +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 EA5DBC954 for ; Sat, 20 Mar 2021 13:27:16 +0100 (CET) Received: from localhost ([::1]:50730 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lNahH-0006K8-VA for larch@yhetil.org; Sat, 20 Mar 2021 08:27:15 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:49302) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lNah0-0006K1-8C for help-guix@gnu.org; Sat, 20 Mar 2021 08:26:58 -0400 Received: from mail1.g12.pair.com ([66.39.4.99]:49563) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lNagr-0005QT-Oh for help-guix@gnu.org; Sat, 20 Mar 2021 08:26:56 -0400 Received: from mail1.g12.pair.com (localhost [127.0.0.1]) by mail1.g12.pair.com (Postfix) with ESMTP id D3C807308A; Sat, 20 Mar 2021 08:26:47 -0400 (EDT) Received: from guix.local (w135107.ppp.asahi-net.or.jp [121.1.135.107]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange ECDHE (P-256) server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mail1.g12.pair.com (Postfix) with ESMTPSA id 21ED0730BE; Sat, 20 Mar 2021 08:26:46 -0400 (EDT) Message-ID: Subject: Re: Bug? coqide missing? (in package coq, version 8.11.2) From: yasu To: Julien Lepiller , help-guix@gnu.org Date: Sat, 20 Mar 2021 21:26:45 +0900 In-Reply-To: <08B18747-D14D-4D0E-91ED-A7E06BCFAA77@lepiller.eu> References: <751596538845b1dc9ec134d0148301f964b44246.camel@yasuaki.com> <08B18747-D14D-4D0E-91ED-A7E06BCFAA77@lepiller.eu> Content-Type: text/plain; charset="UTF-8" User-Agent: Evolution 3.34.2 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Received-SPF: none client-ip=66.39.4.99; envelope-from=yasu@yasuaki.com; helo=mail1.g12.pair.com X-Spam_score_int: -18 X-Spam_score: -1.9 X-Spam_bar: - X-Spam_report: (-1.9 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_NONE=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=1616243237; 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; bh=mo2Xb2pjJAankBtYqSiwm1iWtTFYK6Y9Kwfgi18vS/8=; b=dNA29he/1rIqKoUTGzs3REsrr10bzsZb1QJw5tmXQPRHAMylTlLhfmJPcRZZRfsW30/GOU f8RAntvNly1+aq97H9gNIvB/VG2ewvtgOf3xPtAxxmD7qesHTja1QgzHGhprpOnLeV6/eI UEm85KRBA31BfZZifPN/CYBtSqjJ/iYBV+NBE5mToXviE5nRsQ/faNRutsp/meVhRQL3ZD NpMQwjFd5wknxNPuIgweMrFRSAkRUQq6+L0tcn9aEb2fk0saX34zkS5VMcx3ArEinstqPn CIFWEdobDwd+bYpkaEQdU9K5qrgd7CyhOxYkY7BC7optDcoOK58oAnuHwr9DtA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1616243237; a=rsa-sha256; cv=none; b=jacxg6recbXAqirhPy+WnUO//eJvA1t9kfgfAdgjD9CVruAOTFoIXLBR08X6xFpndwDOFu 9r3PReFyJZvGr31EBL66kF8q9e5RFelgif9N6DCins/V57JW7+FFHmZmUCDVpQcYrnZ3vE 2H4UxXdFZV+Qk38CzNPYoQgJX90QJHahjHipLWsh4KXD1Y0RM5l9JbCIh6pj/bc0ZzaK8x OAAnqm0I7dZjEUybrKIVFS1xYZy4dUX7pAW9dmbmEkuUWee/3hpvsQIfk7BPACP7ogCwiF uskS+g1sX4ZSSSnpDVo79jKnxn0tvdpRriNx4Eo7uS17WX7HUXDV1vw8mdb02Q== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; 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: -2.41 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=none; 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: EA5DBC954 X-Spam-Score: -2.41 X-Migadu-Scanner: scn0.migadu.com X-TUID: OXHxOL43dNBH Hi Julien, Ohhhh, I see, I didn't know anything about these "sub-packages" that follow colon. Is there anything we can do to make it less confusing? One way would be to allow the user to type coqide, or whatever the executable they please, and search for all the possible package names and suggest a way to install an existing package that matches. I imagine something like: > coqide * The command coqide is provided by coq:ide. To install it, run: guix install coq:ide > :-) Yasu On Sat, 2021-03-20 at 06:48 -0400, Julien Lepiller wrote: > Hi Yasu, > > This is not a bug: coqide brings a lot of dependencies, so it's in a > separate output, as you can see with guix search or guix show. To > install it, install the ide output, like so: > > guix install coq:ide > > Le 20 mars 2021 02:11:30 GMT-04:00, yasu a écrit : > > Hello, > > > > After installing COQ using: > > guix install coq > > > > I was perplexed that I could not find the coqide program. > > Howerver, GUIX does seem to build it: > > > > > > ~$ guix build coq > > /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2-ide > > /gnu/store/n8g37cv0028wds959rjgpl5dsj3p3xl0-coq-8.11.2 > > > > ~$ ls /gnu/store/zns66i9iacpkya3mabvygykir5xwl5c4-coq-8.11.2- > > ide/bin > > coqide > > > > > > The fact that this coqide is not brought to user profile - is this > > a > > bug? 😅 > > > > -Yasu > > > >