From unknown Sat Jun 21 05:17:25 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#43248] [PATCH] Fix coqide Resent-From: raingloom Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 06 Sep 2020 18:03:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 43248 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 43248@debbugs.gnu.org X-Debbugs-Original-To: Guix Patches Received: via spool by submit@debbugs.gnu.org id=B.159941533617835 (code B ref -1); Sun, 06 Sep 2020 18:03:01 +0000 Received: (at submit) by debbugs.gnu.org; 6 Sep 2020 18:02:16 +0000 Received: from localhost ([127.0.0.1]:47120 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kEyzY-0004db-5X for submit@debbugs.gnu.org; Sun, 06 Sep 2020 14:02:16 -0400 Received: from lists.gnu.org ([209.51.188.17]:43576) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kEyzV-0004dT-QW for submit@debbugs.gnu.org; Sun, 06 Sep 2020 14:02:14 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:56250) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kEyzV-0003vn-Jc for guix-patches@gnu.org; Sun, 06 Sep 2020 14:02:13 -0400 Received: from mx1.riseup.net ([198.252.153.129]:57830) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kEyzT-0001DG-HY for guix-patches@gnu.org; Sun, 06 Sep 2020 14:02:13 -0400 Received: from bell.riseup.net (bell-pn.riseup.net [10.0.1.178]) (using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits)) (Client CN "*.riseup.net", Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified)) by mx1.riseup.net (Postfix) with ESMTPS id 4Bkzl46twmzFgtP for ; Sun, 6 Sep 2020 11:02:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak; t=1599415329; bh=iUidfmc/AqAZDWaICmaF9lIvbb22mNGR/1o99Z68HKk=; h=Date:From:To:Subject:From; b=ZU08vKN+kfE9cN2UIp2HLFoHrhu7NJTCzVK1uPfOflYkJVHSdDtqET4o0Zqx6Lqdu D9zwfeUWYuqw6YtxtaoFE1ICPIBn44xyCLn5i0+9kb3M1x4Hmy+xTmEz0+BwFfgcup 2laZyX4DFsQByGxNO1sGCoTXqJsbLFiy89vhotDo= X-Riseup-User-ID: 9541A0A06339534F6AD7A2DF4381A17B151C3C631D1A7D5100109BD22C05F9D9 Received: from [127.0.0.1] (localhost [127.0.0.1]) by bell.riseup.net (Postfix) with ESMTPSA id 4Bkzl42tGJzJmvv for ; Sun, 6 Sep 2020 11:02:08 -0700 (PDT) Date: Sun, 6 Sep 2020 20:02:03 +0200 From: raingloom Message-ID: <20200906200203.469c811c@riseup.net> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/KVUUVoFGNDb_Q2/Gh_N=f4/" Received-SPF: pass client-ip=198.252.153.129; envelope-from=raingloom@riseup.net; helo=mx1.riseup.net X-detected-operating-system: by eggs.gnu.org: First seen = 2020/09/06 14:02:09 X-ACL-Warn: Detected OS = Linux 3.11 and newer [fuzzy] X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 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, RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_MSPIKE_H3=-0.01, RCVD_IN_MSPIKE_WL=-0.01, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.4 (-) 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: -2.4 (--) --MP_/KVUUVoFGNDb_Q2/Gh_N=f4/ Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline coqide wasn't working because it couldn't find coqidetop.opt, because it was being deleted due to being a duplicate of coqidetop. I looked at the source to figure out a way to simply convince Coq to use coqidetop, but it would have require too much patching, also other tools might assume either coqidetop or coqidetop.opt being available, so to be safe, I made one into a symlink to the other. Coqide now works without any weird workarounds. --MP_/KVUUVoFGNDb_Q2/Gh_N=f4/ Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0001-gnu-coq-fix-coqide-not-finding-coqidetop.opt.patch >From 2bdebad4adfa78b9c0870341dcc08a36f7ad7734 Mon Sep 17 00:00:00 2001 From: raingloom Date: Sun, 6 Sep 2020 19:11:32 +0200 Subject: [PATCH] gnu: coq: fix coqide not finding coqidetop.opt * gnu/packages/coq.scm (coq) [arguments]: Turn duplicates into symlinks instead of deleting them in remove-duplicate. --- gnu/packages/coq.scm | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 166e66c09e..a0bde5553f 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -96,11 +96,18 @@ (add-after 'install 'remove-duplicate (lambda* (#:key outputs #:allow-other-keys) (let* ((out (assoc-ref outputs "out")) - (bin (string-append out "/bin"))) + (bin (string-append out "/bin")) + (coqtop (string-append bin "/coqtop")) + (coqidetop (string-append bin "/coqidetop")) + (coqtop.opt (string-append coqtop ".opt")) + (coqidetop.opt (string-append coqidetop ".opt"))) ;; These files are exact copies without `.opt` extension. ;; Removing these saves 35 MiB in the resulting package. - (delete-file (string-append bin "/coqtop.opt")) - (delete-file (string-append bin "/coqidetop.opt"))) + ;; Unfortunately, completely deleting them breaks coqide + (delete-file coqtop.opt) + (delete-file coqidetop.opt) + (symlink coqtop coqtop.opt) + (symlink coqidetop coqidetop.opt)) #t)) (add-after 'install 'install-ide (lambda* (#:key outputs #:allow-other-keys) -- 2.28.0 --MP_/KVUUVoFGNDb_Q2/Gh_N=f4/-- From unknown Sat Jun 21 05:17:25 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: raingloom Subject: bug#43248: closed (Re: [bug#43248] [PATCH] Fix coqide) Message-ID: References: <20200907140323.5072311f@tachikoma.lepiller.eu> <20200906200203.469c811c@riseup.net> X-Gnu-PR-Message: they-closed 43248 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 43248@debbugs.gnu.org Date: Mon, 07 Sep 2020 12:04:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1599480242-24108-1" This is a multi-part message in MIME format... ------------=_1599480242-24108-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #43248: [PATCH] Fix coqide which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 43248@debbugs.gnu.org. --=20 43248: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D43248 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1599480242-24108-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 43248-done) by debbugs.gnu.org; 7 Sep 2020 12:03:39 +0000 Received: from localhost ([127.0.0.1]:48305 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kFFs3-0006GI-HY for submit@debbugs.gnu.org; Mon, 07 Sep 2020 08:03:39 -0400 Received: from lepiller.eu ([89.234.186.109]:53970) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kFFs1-0006G8-Gf for 43248-done@debbugs.gnu.org; Mon, 07 Sep 2020 08:03:38 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 146f2b37; Mon, 7 Sep 2020 12:03:35 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:message-id:in-reply-to:references:mime-version :content-type:content-transfer-encoding; s=dkim; bh=4uGpVYhffgog px4w6btnFmX+wXbHEBh1/SyxbZHpLqw=; b=e4PwtrAhrkFltSQf5W22iq4gW0rA xWK0pMBQk6BRCAN28wUS1kviBjKsCYYhHTK0gM5yVysDQHAxVrTu16bzzm1yYVQf klIIozNi2SOfJCy6wg3M5gll2rXN5PCyUygYCjo9j0cHoSRwIM1dgchJU1yv6tyD og5Et9M94I3ZsIEWT0a/P1/g11ZjwSUG6yYOvcoE88TkD9fQTt1DP25WGMVnATvI DxzPZRS5M9CPh8ebousGbYDLeiPBMKHa79pzkNhP/YYG8ehYuvswNt2e5jcwXsHJ j+8D4pza2+ZJFl/67RhUMB1PUkkMpGKJmD2kJcbGW6bgcjRdFzBwsmd2oA== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id df2f7cb8 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Mon, 7 Sep 2020 12:03:34 +0000 (UTC) Date: Mon, 7 Sep 2020 14:03:23 +0200 From: Julien Lepiller To: raingloom Subject: Re: [bug#43248] [PATCH] Fix coqide Message-ID: <20200907140323.5072311f@tachikoma.lepiller.eu> In-Reply-To: <20200906200203.469c811c@riseup.net> References: <20200906200203.469c811c@riseup.net> X-Mailer: Claws Mail 3.17.6 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 43248-done Cc: 43248-done@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 (-) Le Sun, 6 Sep 2020 20:02:03 +0200, raingloom a =C3=A9crit : > coqide wasn't working because it couldn't find coqidetop.opt, because > it was being deleted due to being a duplicate of coqidetop. >=20 > I looked at the source to figure out a way to simply convince Coq to > use coqidetop, but it would have require too much patching, also other > tools might assume either coqidetop or coqidetop.opt being available, > so to be safe, I made one into a symlink to the other. >=20 > Coqide now works without any weird workarounds. Pushed as 1394765238c21030ace4fbb773dc86a9e3c2504c, thank you! ------------=_1599480242-24108-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 6 Sep 2020 18:02:16 +0000 Received: from localhost ([127.0.0.1]:47120 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kEyzY-0004db-5X for submit@debbugs.gnu.org; Sun, 06 Sep 2020 14:02:16 -0400 Received: from lists.gnu.org ([209.51.188.17]:43576) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1kEyzV-0004dT-QW for submit@debbugs.gnu.org; Sun, 06 Sep 2020 14:02:14 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:56250) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kEyzV-0003vn-Jc for guix-patches@gnu.org; Sun, 06 Sep 2020 14:02:13 -0400 Received: from mx1.riseup.net ([198.252.153.129]:57830) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1kEyzT-0001DG-HY for guix-patches@gnu.org; Sun, 06 Sep 2020 14:02:13 -0400 Received: from bell.riseup.net (bell-pn.riseup.net [10.0.1.178]) (using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits)) (Client CN "*.riseup.net", Issuer "Sectigo RSA Domain Validation Secure Server CA" (not verified)) by mx1.riseup.net (Postfix) with ESMTPS id 4Bkzl46twmzFgtP for ; Sun, 6 Sep 2020 11:02:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=riseup.net; s=squak; t=1599415329; bh=iUidfmc/AqAZDWaICmaF9lIvbb22mNGR/1o99Z68HKk=; h=Date:From:To:Subject:From; b=ZU08vKN+kfE9cN2UIp2HLFoHrhu7NJTCzVK1uPfOflYkJVHSdDtqET4o0Zqx6Lqdu D9zwfeUWYuqw6YtxtaoFE1ICPIBn44xyCLn5i0+9kb3M1x4Hmy+xTmEz0+BwFfgcup 2laZyX4DFsQByGxNO1sGCoTXqJsbLFiy89vhotDo= X-Riseup-User-ID: 9541A0A06339534F6AD7A2DF4381A17B151C3C631D1A7D5100109BD22C05F9D9 Received: from [127.0.0.1] (localhost [127.0.0.1]) by bell.riseup.net (Postfix) with ESMTPSA id 4Bkzl42tGJzJmvv for ; Sun, 6 Sep 2020 11:02:08 -0700 (PDT) Date: Sun, 6 Sep 2020 20:02:03 +0200 From: raingloom To: Guix Patches Subject: [PATCH] Fix coqide Message-ID: <20200906200203.469c811c@riseup.net> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/KVUUVoFGNDb_Q2/Gh_N=f4/" Received-SPF: pass client-ip=198.252.153.129; envelope-from=raingloom@riseup.net; helo=mx1.riseup.net X-detected-operating-system: by eggs.gnu.org: First seen = 2020/09/06 14:02:09 X-ACL-Warn: Detected OS = Linux 3.11 and newer [fuzzy] X-Spam_score_int: -27 X-Spam_score: -2.8 X-Spam_bar: -- X-Spam_report: (-2.8 / 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, RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_MSPIKE_H3=-0.01, RCVD_IN_MSPIKE_WL=-0.01, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.4 (-) X-Debbugs-Envelope-To: submit 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: -2.4 (--) --MP_/KVUUVoFGNDb_Q2/Gh_N=f4/ Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline coqide wasn't working because it couldn't find coqidetop.opt, because it was being deleted due to being a duplicate of coqidetop. I looked at the source to figure out a way to simply convince Coq to use coqidetop, but it would have require too much patching, also other tools might assume either coqidetop or coqidetop.opt being available, so to be safe, I made one into a symlink to the other. Coqide now works without any weird workarounds. --MP_/KVUUVoFGNDb_Q2/Gh_N=f4/ Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0001-gnu-coq-fix-coqide-not-finding-coqidetop.opt.patch >From 2bdebad4adfa78b9c0870341dcc08a36f7ad7734 Mon Sep 17 00:00:00 2001 From: raingloom Date: Sun, 6 Sep 2020 19:11:32 +0200 Subject: [PATCH] gnu: coq: fix coqide not finding coqidetop.opt * gnu/packages/coq.scm (coq) [arguments]: Turn duplicates into symlinks instead of deleting them in remove-duplicate. --- gnu/packages/coq.scm | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 166e66c09e..a0bde5553f 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -96,11 +96,18 @@ (add-after 'install 'remove-duplicate (lambda* (#:key outputs #:allow-other-keys) (let* ((out (assoc-ref outputs "out")) - (bin (string-append out "/bin"))) + (bin (string-append out "/bin")) + (coqtop (string-append bin "/coqtop")) + (coqidetop (string-append bin "/coqidetop")) + (coqtop.opt (string-append coqtop ".opt")) + (coqidetop.opt (string-append coqidetop ".opt"))) ;; These files are exact copies without `.opt` extension. ;; Removing these saves 35 MiB in the resulting package. - (delete-file (string-append bin "/coqtop.opt")) - (delete-file (string-append bin "/coqidetop.opt"))) + ;; Unfortunately, completely deleting them breaks coqide + (delete-file coqtop.opt) + (delete-file coqidetop.opt) + (symlink coqtop coqtop.opt) + (symlink coqidetop coqidetop.opt)) #t)) (add-after 'install 'install-ide (lambda* (#:key outputs #:allow-other-keys) -- 2.28.0 --MP_/KVUUVoFGNDb_Q2/Gh_N=f4/-- ------------=_1599480242-24108-1--