Company-coq shows two doc buffers

[santifa]

Hey folks,

I use emacs 26.2 with the development version of spacemacs.
The autocompletion works fine but two doc buffers are opened when the documentation of some element is shown. One doc buffer is the original one generated from
company-coq and the other is the company-quickhelp pos-tip window which should subsume
the doc buffer.

I use the orginal spacemacs configuration for coq.
What further informations could help or any suggestions?

[cpitclaudel]

Hi there,

It's a known issue: the problem is that company-quickhelp requests a documentation buffer and reads its contents to know what to display. Unlike many other packages, company-coq doesn't just return the doc buffer, it also displays it (that's not a bug; I have to do it that way because otherwise I can't set up the appropriate html rendering).

I merged a fix in company-quickhelp for that a while ago; see company-mode/company-quickhelp#71 ; but I haven't had the time to update company-coq accordingly, in large part because company-quickhelp doesn't work well with very long documentation strings, like those returned by company-coq for tactics. For symbols, types would fit in a company-quickhelp popup, but sometimes Coq is slow to print a type out (because types can be very large).

So, short-term, the fix is to disable company-quickhelp in Coq mode. medium-term, a fix would be to use quickhelp-string (see the PR above) instead of doc-buffer, and restrict it to just some completion backends. Long-term, porting company-coq's documentation to use the new Sphinx manual would give us much shorter docstrings that we could feed to company-quickhelp.

I don't think I'll have time to work on either of these last two soon, but I'd be happy to mentor patches in the direction of the medium or long-term solutions.

HTH.