Comments (10)
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.
Related Issues (20)
- Is it really necessary to pop up the output panel when typechecking a file? HOT 18
- Ignore screenshots when release a new version
- More safe way to get document object
- v0.9.8 broken on Windows HOT 18
- "Generate initial pattern match clause" doesn't respect multiline signatures
- "Generate initial pattern match clause" doesn't respect LIDR syntax
- New lines are incorrect for some multi-line hints
- `idris.typecheck` command stops working HOT 8
- I think my settings are wrong. - 'idris.typecheck' HOT 2
- Default Keyboard Shortcuts HOT 3
- line number and column snippet is not shown when evaluating idris code
- How to use packages?
- make-lemma seem don't work
- Output channel is focused HOT 2
- Cannot run extension on Windows HOT 7
- suggestions appear before quickSuggestionDelay
- Cannot search or install this plugin anymore through vscodium marketplace HOT 1
- Support idris2 HOT 4
- After type checking error ("didn't load"), hovering messages becomes confusing
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from vscode-idris.