Hovering over contents of a new takes about one minute

[xiaopong]

After opening a file in editor, hovering over a function name only sees the message "loading...", it takes about a minute to finally see the type information, and during this time, the chezscheme processing running idris2.so is spinning CPU at 100%.

The same behavior happens regardless of whether the Hover Action is set to "Type Of" or "Type At". However, when the hover action is set to "Type At", hovering over certain locally defined function would trigger the loading issue every time. I have not been able to reproduce the issue on all locally defined functions though.

Environment: Idris 2, version 0.4.0-f77670814 idris-vscode v.0.0.9

Maybe it's a version mismatch between idris2 and idris-vscode?

[meraymond2]

It sounds like an issue with the idris2 process starting. Can you run idris2 --ide-mode --find-ipkg in the project directory and see what it outputs?

[timsueberkrueb]

Hey, I have the same issue. Running idris2 --ide-mode --find-ipkg gives the expected output:

> idris2 --ide-mode --find-ipkg
000018(:protocol-version 2 0)

Is there something else I can try in order to debug this? Thanks!

[meraymond2]

Are you also using 0.4.0, and do you have an example of a repo where this is happening?

I'm testing on the Idris2 repo because most people have that, but it's a bit problematic because the idris2 --ide-mode --find-ipkg command is confused by the two ipkgs files, but if I temporarily remove the idris2api.ipkg file, it works. I'm using 0.4.0, from the Nixos unstable channel.

The best way to test is to clone this repo, change line 76 in src/state.ts to debug: true and rebuild it. The readme has instructions for running locally. In the debug console in VS you will be able to see all of the messages that go to and from and ide-process.

<< 00003e((:load-file "/home/michael/dev/Idris2/src/Core/Hash.idr") 1)

>> (:protocol-version 2 0)
>> ...lots of source highlighting messages

If it's not working for some reason, like the ipkg thing, it won't show anything after the :load-file message.

[timsueberkrueb]

Thanks! This is a snippet where I can reproduce it and I've made a screencast of the issue:

https://user-images.githubusercontent.com/11774614/124507930-209c1200-ddcf-11eb-9e6a-b5d5428aa337.mp4

First I hover over example and it works just fine. Next, I hover over the colon in the type definition of example. Afterwards, the CPU load goes up and it gets unresponsive.

I'm running Ubuntu 20.04 and I've built Idris 2 from source (v0.4.0 tag).

[timsueberkrueb]

I just tested #60, and it actually seems to fix this issue for me!

[meraymond2]

That's really helpful, thanks for making that.

Looking at it, it might have been that bug after all. In the worst case when you hover between words, it was trying to type check the whole document, and then got stuck.

[Dessix]

60 was a bug in that it was evaluating both the early-out code-paths and the long-form code paths, but returning immediately regardless. I do believe, however, that there's still a bug- the final res(...) lines should either be returned or awaited as well.

This, however, will mean that the promise in question won't insta-return, and something may currently be relying on that bug to function.

Edit: Disregard this- I misread the PR context, and assumed res was a promise-function, not the constructor to Promise's resolve callback. Too much time spent with Rust futures ^^;

[meraymond2]

That fix is released in the 0.0.10 version.