Speed up checking about vscode-idris HOT 10 CLOSED

Hi, @ndmitchell Currently there is no reload command in Idris IDE protocol, and yes the :load-file command will load the file from scratch each time:

But the loading time on my side is relatively acceptable, do you work with an iPKG based Idris project or a standalone Idris file? Can you give me the code snippets which you found the loading time is quite long? Thanks in advance!

from vscode-idris.

Probably we should fire an issue for this on Idris upstream repository.

from vscode-idris.

I work with idris.exe on Windows 10, downloaded from the website and unpacked (not compiled). I'm working on a single Idris file, namely:

module Hello

hello : String
hello = "test"

After hitting Ctrl S to save it takes 4 seconds for the output to return to "File loaded successfully". To :load the file in the Idris interactive environment takes < 1s (around 0.4s). To :reload the file takes perhaps 0.2s. So it may not be :load-file, but might be something else. Is there any way to get more detailed timings of how long the individual steps take?

from vscode-idris.

Sorry for the delay, I will do some investigation here.

from vscode-idris.

Hi @ndmitchell, sorry for the huge delay. I look at this issue again and find out the reason under the hood. The extension will kill the Idris process every time when the typechecking process succeeds because of this issue here #52, so basically, you have to wait for the Idris process getting up again every time when you run the typechecking command, that will cost you around 2-3 seconds.

from vscode-idris.

Perhaps kill the Idris process every N evaluations, where N is ~1000 or similar?

from vscode-idris.

@ndmitchell Good idea, I will do that, and the N will also be configurable then.

from vscode-idris.

@ndmitchell 1000 times is too large for this, the memory leaking issue will happen every 50 times of continuous type checking I guess, so I set the default continues type checking times to 10 here.

from vscode-idris.

Do you still think that adding a reload command to IDE protocol is useful?

from vscode-idris.

@clayrat Yes, I think so. I'm not familiar the underlying implementation of IDE protocol, but a reload command is mandatory indeed, besides that the IDE protocol need to add more generalized type-of and docs-for command to get information about local identifiers and the repl-completion need some performance optimization and need to return the kind of the identifiers e.g. function, variable or type as mentioned here #31.

from vscode-idris.