Idris2 support
Opened this issue · 6 comments
I'm creating this to track the implementation of Idris2 support.
The dream is that the same client would be compatible with both 1 and 2, but at this time I'm not sure how different the protocol is. Since Idris2 is supposed to be mostly backwards compatible, I think it makes sense to keep the clients unified, if possible.
Need to also confirm how stable the v2 protocol is — if its likely to change frequently, it might be worth keeping separate for now.
Idris 2 Command Implementation
Anything that's blank is unimplemented, but will not crash the client. Basically they're just empty, ok replies.
-
:add-clause -
:add-missing— impossible as long as missing cases won’t load -
:apropos -
:browse-namespace -
:calls-who -
:case-split -
:docs-for— working, but no metadata yet -
:generate-def -
:generate-def-next -
:interpret— working, but different result -
:load-file— working, but different behaviour if code has errors -
:make-case -
:make-lemma— implemented, but a little broken -
:make-with -
:metavariables -
:print-definition -
:proof-search -
:proof-search-next -
:repl-completions -
:type-of— working, slightly different response (includes namespace in var name) -
:version -
:who-calls
Before I get to worry about protocol changes, I need to fix process termination.
When the Idris1 process receives a SIGQUIT EOF it prints
000036(:return (:error "<stdin>: hGetChar: end of file") 0)
Idris2 prints
Alas the file is done, aborting
which breaks the lexer.
I might try and figure out what's causing that message to print, because ideally the IDE should only ever use the protocol to communicate. Failing that, we can give the client a shutdown method that would tell it to stop listening in advance of the process being killed.
I don't want to change the lexer, I like it being simple and only handling the protocol messages.
Idris2 prints
Alas the file is done, aborting
I would consider this a bug in idris2 and we should report that.
While adding v2 tests, I've noticed a few other cases where the reply looks wrong, or it's slightly different than it was before. I'm going to make separate issues for anything that might be a bug. And there are still lots of unimplemented commands, and metadata/highlighting isn't implemented yet.
My primary goal is to get the client/plugins in a usable state with v2. So nothing should make the client crash, and it should gracefully handle some missing information, like the metadata.
It's a bit annoying that the return type for unimplemented commands isn't consistent. Some are empty, successful:returns with an additional :write-string message, but a few are :error returns. I'm not sure yet if there are any changes necessary in the client to enable the plugins to handle missing commands gracefully.
Raised an issue for the EOF error: idris-lang/Idris2#394
While testing that, I noticed that the output of idris2 --ide-mode-socket has changed too, it prints the REPL header now.
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.2.0
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
38398
and, the stdout is buffered, so the callback doesn't get called. You can see this if you run idris2 --ide-mode-socket > out, it won't flush until you quit the process. Sigh.
Just an update, I've made an issue that details all the little breaking changes that aren't exactly bugs, so I've closed some of the command-specific tracking issues. Also, the latest version 0.2.1 has implemented some more commands, so I've ticked them in the list.
I still need to make an issue for the socket bug I described above, or at the least figure out a workaround for the examples.
The socket bug has at least been fixed.
The EOF bug is definitely still there, but somehow it's stopped causing problems for the client, and I'm not sure why.