Display tooltips correctly (when loc is None) #17012
Conversation
coqbot-app
bot
added
the
needs: full CI
| let start, stop = match loc with | ||
| | None -> start_sentence, stop_sentence | ||
| | Some loc -> | ||
| (* FIXME: tooltips don't show correctly for this case *) |
There was a problem hiding this comment.
@ejgallego The explanation provided by Jim is that your last commit in your PR reintroduces a performance issue:
The last commit ("Fix bizarre location-handling code.") reintroduces the O(n^2) behavior. The ones before it are OK. (Pff.v, a 1.2 MB file, takes about 3 minutes to run in CoqIDE both on master and with the first 3 commits. With the 4th commit, I gave up after 10 minutes, and it had only processed half the source.)
So the point of this PR is supposed to be: fix the tooltip issue without reintroducing the quadratic behavior.
Note that I'm just commenting based on my reading of the comments, I haven't looked at the actual code on either PR.
There was a problem hiding this comment.
I'll have a look into the performance issue, but it is not introduced in the code part this PR is touching, the last commit in the PR does indeed touch 2 different code paths.
I'll split the commit in two. This PR still makes little sense as we have better code for the Some path in the other PR, whereas this one just puts some code that looks pretty strange.
There was a problem hiding this comment.
I fail to see the point of this PR
The issue is unrelated to your original PR. I took the part of your changes that made sense. Currently, no warning uses the code for the Some branch, and IIRC your code was not correct for the Some case. I assumed it was urgent to get your other code into 8.17 and that we should fix the tooltip problem in 8.17. Fixing the Some case doesn't have to be in 8.17, though I planned to look at it very soon. Now I'm not sure I should bother.
There was a problem hiding this comment.
My code was almost correct for the Some case, it only did mishandle the case where UTF-8 symbols where before in the buffer, whereas the current code here mishandles all of them. Moreover it was noted as a fixme which is now fixed.
Indeed, why you would like to spend time fixing something that is already fixed is an interesting question.
Note that when taking parts of the code of some other developer, it may sensible to ask them first what are they planning to do with it, otherwise you risk indeed doing double work.
By the way, you should be able to hit the Some case, at least quite a few warnings do set ?loc , then why the feedback may be discarded at the STM level is a different issue.
I think having better tests is much welcome in this area.
github-actions
bot
added
the
needs: rebase
|
Original PR improved and merge. Thanks a lot @jfehrle for all the comments and testing. We may want to open a new bug for the tooltips that are lost due to "detached" feedback (but that's a way harder issue to fix) |
Fixes: #16987
The case where
locisNoneis the important one--none of the calls toCWarnings.createpassloc. I haven't figured out the fix for theSomecase yet. IMO that's not urgent, though I will work on it in the next few days.Error messages also generate tooltips. These seem to work correctly even when
locis provided. FWIW, I found 79 places in the source of errors that can provideloc.Attn: @Zimmi48 @ejgallego