Bug#946580: No coqidetop in coq package breaks editor plugins

[Julien Lepiller <julien@lepiller.eu>]

Le 11 décembre 2019 21:54:54 GMT+01:00, Ralf Treinen <treinen@free.fr> a écrit :
>Hello,
>
>On Wed, Dec 11, 2019 at 10:31:57AM +0100, Julien Lepiller wrote:
>> Package: coq
>> Version: 8.9.0-1
>> 
>> Hi, sorry in advance if my message is not formated correctly. I'm not
>a debian user, but I'm trying my best :)
>
>your bug report is fine, don't worry ;-)
>
>> I'm the developer of a coq plugin in neovim called coquille. One of
>my users reported a failure at starting the plugin due to coq not being
>found, although the package was installed. We have determined that the
>issue was caused by the absence of coqidetop, although they had coq 8.9
>installed.
>> 
>> 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.
>
>coq 8.9.0 had building of the coqide switched off, and as a consequence
>there
>was no coqide package for that version. I am currently working on
>updating
>the coq package to version 8.10.2, including a coqide package. That
>package
>will also include the coqidetop binary. I hope to upload the package
>in the next days, but then it will have to be accepted by the ftp
>masters
>before it will be visible in unstable, and I don't know how long that
>will take.
>
>-Ralf.

Hi,

Thanks for thc answer. So it's going to be fixed.

I want to suggest putting coqidetop in the coq package, because it's not a graphical tool and it is generally useful to coq users, not only coqide users. I don't think it requires lablgtk or graphics libraries, which is the only reason I can see behind a split of the coq package.