Bug 1791377 - No coqidetop in coq package breaks editor plugins
Summary: No coqidetop in coq package breaks editor plugins
Keywords:
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: coq
Version: 31
Hardware: Unspecified
OS: Unspecified
unspecified
unspecified
Target Milestone: ---
Assignee: Alan Dunn
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2020-01-15 16:53 UTC by vaxefo7623
Modified: 2020-01-25 06:34 UTC (History)
2 users (show)

Fixed In Version: coq-8.9.1-5.fc31
Clone Of:
Environment:
Last Closed: 2020-01-25 06:34:53 UTC
Type: Bug
Embargoed:


Attachments (Terms of Use)

Description vaxefo7623 2020-01-15 16:53:53 UTC
Description of problem:
I'm the developer of a coq plugin in neovim called coquille. Even though coq 8.9 is installed on my Fedora workstation, I cannot use the plugin due to the absence of coqidetop.

Before coq 8.9, I could use coqtop with the -ide-slave option. That option is now replaced by a separate binary, coqidetop, that I need in order to evaluate coq expressions from my plugin.

Version-Release number of selected component (if applicable):
8.9 and above

Actual results:
coqidetop is not found, since it's not packaged in the coq package.

Expected results:
coqidetop is not related to coqide, the graphical coq IDE. It is really similar to coqtop, but with support for other IDEs. It's really small and should be part of the coq package, not the coq-coqide package (which should only provide the coq IDE).

Additional info:
I previously reported it to Debian since they had the same issue and they fixed it: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=946580

The situation in debian was worse since they didn't build coqide and had no coqidetop binary at all. At least installing coqide is a work-around in Fedora, even though it installs unneeded graphical libraries and a useless IDE :).

Comment 1 Jerry James 2020-01-15 20:42:42 UTC
Thanks for the report.  I will fix that today.

Comment 2 Fedora Update System 2020-01-16 21:39:49 UTC
coq-8.9.1-5.fc31 has been pushed to the Fedora 31 testing repository. If problems still persist, please make note of it in this bug report.
See https://fedoraproject.org/wiki/QA:Updates_Testing for
instructions on how to install test updates.
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2020-41b62b9e3f

Comment 3 Fedora Update System 2020-01-25 06:34:53 UTC
coq-8.9.1-5.fc31 has been pushed to the Fedora 31 stable repository. If problems still persist, please make note of it in this bug report.


Note You need to log in before you can comment on or make changes to this bug.