GNU bug report logs - #43248
[PATCH] Fix coqide

Previous Next

Package: guix-patches;

Reported by: raingloom <raingloom <at> riseup.net>

Date: Sun, 6 Sep 2020 18:03:01 UTC

Severity: normal

Tags: patch

Done: Julien Lepiller <julien <at> lepiller.eu>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 43248 in the body.
You can then email your comments to 43248 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

View this report as an mbox folder, status mbox, maintainer mbox

Report forwarded to guix-patches <at> gnu.org:
bug#43248; Package guix-patches. (Sun, 06 Sep 2020 18:03:01 GMT) Full text and rfc822 format available.
Acknowledgement sent to raingloom <raingloom <at> riseup.net>:
New bug report received and forwarded. Copy sent to guix-patches <at> gnu.org. (Sun, 06 Sep 2020 18:03:02 GMT) Full text and rfc822 format available.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: raingloom <raingloom <at> riseup.net>
To: Guix Patches <guix-patches <at> gnu.org>
Subject: [PATCH] Fix coqide
Date: Sun, 6 Sep 2020 20:02:03 +0200

[Message part 1 (text/plain, 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.

[0001-gnu-coq-fix-coqide-not-finding-coqidetop.opt.patch (text/x-patch, attachment)]
Reply sent to Julien Lepiller <julien <at> lepiller.eu>:
You have taken responsibility. (Mon, 07 Sep 2020 12:04:02 GMT) Full text and rfc822 format available.
Notification sent to raingloom <raingloom <at> riseup.net>:
bug acknowledged by developer. (Mon, 07 Sep 2020 12:04:02 GMT) Full text and rfc822 format available.

Message #10 received at 43248-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: raingloom <raingloom <at> riseup.net>
Cc: 43248-done <at> debbugs.gnu.org
Subject: Re: [bug#43248] [PATCH] Fix coqide
Date: Mon, 7 Sep 2020 14:03:23 +0200

Le Sun, 6 Sep 2020 20:02:03 +0200,
raingloom <raingloom <at> riseup.net> a écrit :

> 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.

Pushed as 1394765238c21030ace4fbb773dc86a9e3c2504c, thank you!
bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Tue, 06 Oct 2020 11:24:06 GMT) Full text and rfc822 format available.
This bug report was last modified 3 years and 202 days ago.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.