Speed up checking

[ndmitchell]

Having experimented with checking in VS Code, versus having the Idris interactive editor open, I found the interactive editor for :r was instant, but the Idris plugin is pretty slow. Is that because it's reloading from scratch each time? Any way to speed it up?

[zjhmale]

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!

[zjhmale]

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

[ndmitchell]

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?

[zjhmale]

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

[zjhmale]

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.

[ndmitchell]

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

[zjhmale]

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

[zjhmale]

@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.

[clayrat]

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

[zjhmale]

@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.