From unknown Sat Jun 21 03:04:34 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#43248 <43248@debbugs.gnu.org> To: bug#43248 <43248@debbugs.gnu.org> Subject: Status: [PATCH] Fix coqide Reply-To: bug#43248 <43248@debbugs.gnu.org> Date: Sat, 21 Jun 2025 10:04:34 +0000 retitle 43248 [PATCH] Fix coqide reassign 43248 guix-patches submitter 43248 raingloom severity 43248 normal tag 43248 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Sun Sep 06 14:02:16 2020 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/-- From debbugs-submit-bounces@debbugs.gnu.org Mon Sep 07 08:03:39 2020 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! From unknown Sat Jun 21 03:04:34 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Tue, 06 Oct 2020 11:24:06 +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