RFC: IDE Mode protocol rework
Opened this issue · 20 comments
IDE mode works by sending/receiving messages on the wire in the form of
s-expressions (lists, strings, bools, integers, symbols). Currently, almost
all the commands are implemented by delegating the processing to the same
machinery that handles REPL commands and dump the formatted output string to a
single string message. As IDE mode is intended to be used by machine and not
humans, we can ditch formatted string output and add more structured information to be
used by clients. It makes no sense for the editors to first parse the s-expression and
then have to reparse a string with an undefined syntax to display information more accurately
than simply dumping the response in a buffer or statusline.
The aim of this proposal is not changing the language of the
request/messages, but the structure of the response, adding additional
information to be used by the client and producing a complete documentation for
the commands.
Suggestions and even strong opinions on the format of the messages are highly appreciated.
Next there will be a section for each command with the structure of the
request and the structure of a successful response. At the bottom there is a
separate section for warning/error messages and additional non request related
messages.
Warning: These will be a lengthy proposal that is also intended as starting point for documentation.
Language of the messages
The datatype associated to the language is defined in
src/Idris/IDEMode/Commands.idr:13. Here I provide the translation of
s-expressions to string, as a reference for the next sections.
SymbolAtom "symbol" => :symbol
IntegerAtom 42 => 42
BoolAtom True/False => :True/:False
StringAtom "string" => "string"
SExpList [c1, c2, c3] => (c1 c2 c3)
Interpret
Interprets, as in the REPL, a single expression:
Current:
((:interpret "expr") req-id) -> (:return (:ok "res") req-id)
Proposed:
((:interpret "expr") req-id) -> (:return (:ok (:expr "res") (:type "type")) req-id)
Example:
((:interpret "plus 40 2") 1) -> (:return (:ok (:expr "42") (:type "Nat")) 1)
Additional points:
- information on the request expression, e.g. the typing?
- option for execution instead of interpretation?
LoadFile
Loads the provided file as main file to be typechecked. Declarations and
imported modules are available for interpretation. Particularly relevant since
editing commands require that the file is loaded both the first time and after
each modification.
Current:
((:load-file "path" ()) req-id) -> (:return (:ok ()) req-id)
((:load-file "path" line) req-id) -> (:return (:ok ()) req-id)
No changes required, however currently the line number is always ignored by the
compiler and it can print additional messages like in the REPL in the form of
(:write-string "Building Module(path)").
TypeOf
Current:
((:type-of "name") req-id)
-> (:return (:ok ("namespace.name : type\nnamespace2.name : type")) req-id)
((:type-of "hole") req-id)
-> (:return (:ok (" n1 name1 : type1\n n2 name2 : type2\n----------------------\nhole : type")) req-id)
((:type-of "name" line col) req-id) -> same as previous
Proposed:
((:type-of "name") req-id)
-> (:return (:ok (((:name "namespace.name") (:type "type")) ... ((:name "namespacen.name") (:type "type"))) req-id)
((:type-of "hole") req-id)
-> (:return (:ok (((:mult "n1") (:name "name1") (:type "type1")) ... ((:mult "nn") (:name "namen") (:type "typen")) ((:name "name") (:type "type"))) req-id))
((:type-of "name" line col) req-id) -> same as previous
Example:
((:type-of "foo") 1) -> (:return (:ok ((:name "Main.foo") (:type "List Nat")) ((:name "Bar.foo") (:type "Vect n Nat"))) 1)
((:type-of "hole") 1) -> (:return (:ok ((:mult 0) (:name "a") (:type "Type")) ((:mult 1) (:name "x") (:type "Nat")) ((:name "Main.hole") (:type "Bool"))) 1)
CaseSplit
Current:
((:case-split line "name") req-id)
-> (:return (:ok "name x y = ?hole1\nname x z = ?hole2") req-id)
((:case-split line col "name") req-id) -> same as previous
Proposed:
((:case-split line "name") req-id)
-> (:return (:ok ((:line l) (:expr "name x y = ?hole1")) ... ((:line l) (:expr "name x z = ?hole2))) req-id)
((:case-split line col "name") req-id) -> same as previous
Example:
((:case-split 4 "xs") 1) -> (:return (:ok ((:line 4) (:expr "foo [] = ?foo_rhs1")) ((:line 5) (:expr "foo (x :: xs) = ?foo_rhs2"))) 1)
Additional points:
- Can we assume that always the whole line is modified by a case-split and that the compiler does not touch other non-related text in the lines?
AddClause
Current:
((:add-clause line "name") req-id)
-> (:return (:ok "name x y = ?hole1") req-id)
Proposed:
((:add-clause line "name") req-id)
-> (:return (:ok ((:line l) (:expr "name x y = ?hole1"))) req-id)
Example:
((:add-clause 4 "foo") 1) -> (:return (:ok ((:line 5) (:expr "foo xs = ?foo_rhs1"))) 1)
Additional points:
- The compiler correctly returns the correct amount of whitespaces for local-declarations
indentation or it should provide a col field in the response and let the editor handle it?
AddMissing
NOT IMPLEMENTED YET
#### ExprSearch
Current:
((:proof-search line "name") req-id)
-> (:return (:ok "expr") req-id)
((:proof-search line "name" ("hint1" ... "hintn")) req-id)
-> (:return (:ok "expr") req-id)
((:proof-search line "name" ("hint1" ... "hintn") :all) req-id)
-> (:return (:ok "expr1\n...\n\exprn") req-id)
Proposed:
((:proof-search line "name") req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) ((:expr "expr"))) req-id)
((:proof-search line "name" ("hint1" ... "hintn")) req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) ((:expr "expr"))) req-id)
((:proof-search line "name" ("hint1" ... "hintn") :all) req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) ((:expr "expr1") (:expr "expr2"))) req-id)
Example:
((:proof-search 5 "todo") 2) -> (:return (:ok (:start-line 2) (:start-col 14) (:end-line 2) (:end-col 18) ((:expr "S Z"))) 2)
((:proof-search 5 "todo") 2) -> (:return (:ok (:start-line 2) (:start-col 14) (:end-line 2) (:end-col 18) ((:expr "S Z") (:expr "Z"))) 2)
ExprSearchNext
Current:
((:proof-search-next) req-id) -> (:return (:ok "expr") req-id)
Proposed:
((:proof-search-next) req-id) -> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) (:expr "expr")) req-id)
Example:
((:proof-search-next) 2) -> (:return (:ok (:start-line 2) (:start-col 14) (:end-line 3) (:end-col 23) ((:expr "Z"))) 2)
Additional points:
- This command is particularly tricky since currently it only outputs the new search result,
and is tricky for editors to figure where to replace this new expression.
GenerateDef
Current:
((:generate-def line "name") req-id)
-> (:return (:ok "expr") req-id)
Proposed:
((:generate-def line "name") req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) ((:expr "expr"))) req-id)
((:generate-def line "name" :all) req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) ((:expr "expr1") (:expr "expr2"))) req-id)
Example:
((:generate-def 5 "foo") 2) -> (:return (:ok (:start-line 6) (:start-col 1) (:end-line 6) (:end-col 1) ((:expr "foo x = S Z"))) 2)
Additional points:
- This command is the same as a AddClause + ExprSearch, it should behave in the same manner.
GenerateDefNext
Current:
((:generate-def-next) req-id)
-> (:return (:ok "expr") req-id)
Proposed:
((:generate-def-next) req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) ((:expr "expr"))) req-id)
Example:
((:generate-def-next) 2) -> (:return (:ok (:start-line 6) (:start-col 1) (:end-line 7) (:end-col 1) ((:expr "foo Z = Z"))) 2)
MakeWith/MakeCase
Current:
((:make-with line "name") req-id)
-> (:return (:ok "expr") req-id)
Proposed:
((:make-with line "name") req-id)
-> (:return (:ok (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) (:expr "expr")) req-id)
Example:
((:make-with 5 "foo") 2) -> (:return (:ok (:start-line 6) (:start-col 1) (:end-line 6) (:end-col 1) (:expr "foo x with (_)\n foo x | with_case = ?foo_rhs1")) 2)
MakeLemma
Current:
((:make-lemma line "name") req-id)
-> (:return (:ok "expr") req-id)
Proposed:
((:make-lemma line "name") req-id)
-> (:return (:ok (:line l) (:expr "expr")) req-id)
Example:
((:make-lemma 12 "lemma") 2) -> (:return (:ok (:line 8) (:expr "lemma : Bool -> Bool")) 2)
Additional point:
- The line in the output is needed to know where it is safe to put the new definition.
DocsFor
Current:
((:docs-for "name") req-id) -> (:return (:ok "very length docs with sections") req-id)
((:docs-for "name" :overview) req-id) -> (:return (:ok "very length docs with sections") req-id)
((:docs-for "name" :full) req-id) -> (:return (:ok "very length docs with sections") req-id)
Proposed:
((:docs-for "name") req-id)
-> (:return (:ok (:name "namespace.name") (:type "type") (:section "section name" ...) req-id)
Example:
((:docs-for "Nat") 2) -> (:return (:ok (:name "Prelude.Nat") (:type "Type") (:section "Description" "...") (:section "Constructors" ((:name "S") (:type "Nat -> Nat") (:doc "...")) ((:name "Z") (:type "Nat") (:doc "..."))) ...) 2)
Additional points:
- Documentation sections are not uniform between constructs (i.e. interface vs data types), we can be strict on the section types and arguments
or more liberal, like in the proposal, and let the editor handle it.
Apropos
NOT IMPLEMENTED YET
Whocalls
NOT IMPLEMENTED YET
Callswho
NOT IMPLEMENTED YET
BrowseNamespace
Current:
((:browse-namespace "name") req-id) -> (:return (:ok "very length docs with sections") req-id)
Proposed:
((:browse-namespace "name") req-id)
-> (:return (:ok (:name "name") ((:name "name") (:type "type")) ...) req-id)
Additional points:
- We display only the name and the type or we can add descriptive fields?
Metavariables
Current:
((:metavariables) req-id) -> (:return (:ok (("name" ((" n name" "type" ()) ...) ("type" ())))) req-id)
Proposed:
((:metavariables) req-id)
-> (:return (:ok ((:name "hole") (:line l) (:col c) (((:mult "n1") (:name "name1") (:type "type1")) ... ((:mult "nn") (:name "namen") (:type "typen")) ((:name "name") (:type "type")))) ...) req-id)
Additional points:
- Just return the list of metavariables and require a new TypeOf command to fetch the metavariable context?
NormaliseTerm
NOT IMPLEMENTED YET
ShowTermImplicits
NOT IMPLEMENTED YET
HideTermImplicits
NOT IMPLEMENTED YET
ElaborateTerm
NOT IMPLEMENTED YET
PrintDefinition
NOT IMPLEMENTED YET
ReplCompletions
NOT IMPLEMENTED YET
Other responses and notes
Warning current:
(:return (:warning "warning") req-id)
Warning proposed:
(:return (:warning ((:filename "file") (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) (:msg "msg") (:hint "hint")) ...) req-id)
Error current:
(:return (:error "error") req-id)
Error proposed:
(:return (:error ((:filename "file") (:start-line l1) (:start-col c1) (:end-line l2) (:end-col c2) (:msg "msg") (:hint "hint")) ...) req-id)
Additional messages: (:write-string "string" req-id)
Syntax output: (:output ... req-id)
Protocol version: (:version major minor)
- Both warning and errors dumps the same string that the compiler outputs to stdout when calling it from terminal.
- There should be an option to disable additional messages (i.e. when the reloading requires the recompilation of an imported module).
- Top-level declaration can have a multiplicity, should we add also a field for that when searching and in docs?
- How can we guarantee future proofing for more arguments in current commands: specify a supported version in initialization?
Add a possibile:extrakeyword to be specified? - Should the output be already formatted or that must be handled only by the editor?
Implementation
Modification can be implemented as a next minor version that can be required during initialization or we can provide a legacy layer to be enabled
via a command-line option until we can deprecate and retire the old protocol version.
Additional commands are not discussed in this proposal, but ideally they should obey the same rationale behind these changes.
CaseSplit
Can we assume that always the whole line is modified by a case-split and that the compiler does not touch other non-related text in the lines?
No, this has been a source of bugs when using case-split in lambda-case and in with-patterns. There should be a way for the editor to know which part of the AST has been modified and which must remain intact (in this case the rhs must remain the same)
AddClause
The compiler correctly returns the correct amount of whitespaces for local-declarations
indentation or it should provide a col field in the response and let the editor handle it?
It should return a number of columns. In my view the compiler should not concern itself with layout or presentation and should only return "structure". Typically editors might bet set to use tabs instead of spaces, or might have a different indentation level by default (for accessibility reasons), which the compiler is unaware of and would break by returning preformated output.
Notes
Both warning and errors dumps the same string that the compiler outputs to stdout when calling it from terminal.
Sounds like this could be improved but I wouldn't fret about it too much in the short term. Ideally in the future there should be precise positional information about which part is wrong and which other part caused it.
Modification can be implemented as a next minor version that can be required during initialisation or we can provide a legacy layer to be enabled.
Versioning the protocol is actually a great idea. We could have every command ask which version of the protocol its talking so that we can iterate on the protocol until it reaches a satisfactory state. (Ideally the protocol should also be generic enough for other programming langauges but that's a talk for another time)
Is there a reason not to use Language Server Protocol? It seemed to work for Haskell with haskell-language-server so I would assume it would work for Idris 2 as well.
There is, but the reason is hypothetical as for now. There is some level of concern about the LSP not being flexible enough to encode all planned (but mostly theoretical) features we may want the Idris 2 IDE protocol to support. I must tell that I don't know much about and haven't looked into the LSP specs by now. So all I just said is based on what I've heard.
But at the moment, I don't think we have anything in the protocol that requires strictly more power than LSP provides us. At least the current functionality is fairly modest and it feels like LSP can definitely handle that 😅
Please correct me if I'm wrong here.
@Russoul I'm not sure what could be limiting about LSP. I would assume that anything not covered by the LSP spec could be a custom command. I do not know a lot about LSP so I could be wrong.
I'm also exploring the possibility of a LSP server implementation with maybe some more functionalities, but definitely it would be a distinct project from the compiler effort, so I've not opened a related issue.
@ShinKage This could be a silly question, but why not implement LSP directly in the compiler? If the goal of --ide-mode is to talk to IDEs, why not pick a protocol they already support?
The reasons are pretty boring:
- workforce: until recently only edwin was working on Idris2 and the community is small so nobody got around to it.
- expertise: I don't know anyone in the community who's got time and skill to implement LSP and other people to review and test the implementation
- compatibility: LSP is only one way, compiler -> server, but the IDE-mode is two ways, source -> compiler -> source, if you're gonna implement all the unique features of idris like code synthesis and automatic case split, you indeed would have to implement them as an LSP extension. Which completely defeats the purpose of using LSP in the first place since the language is effectively "broken" without those features.
Those aren't very good reasons, and LSP should definitely be implemented in some shape of form, but this is a research project with very limited resources, so we make do with what we have!
There is an argument to be made about either designing a "theorem prover LSP extension" or upstreaming our changes needed so LSP can perform syntax tree modifications but those require, you guessed it, people and expertise!
All that is to say: contributions are welcome (and needed!) :)
Adding to what @andrevidela said, I think LSP can potentially handle all the functionalities we currently have and more, however it may need some additional plugin from the editor side to integrate them seamlessly like (partially) the idris plugin, or the agda emacs mode. Nonetheless I'm starting to believe that a LSP server would be really helpfull even if we have a custom IDE mode due to the large support from the major editors and the fact that associated tooling would probably already known from newcomers to Idris2.
Regarding the compiler integration, IIRC @edwinb said previously that additional tooling (for example a more powerful REPL) should be in a separate repo, and I agree. Manpower is low currently, and adding additional tooling to the repo would translate to even more stuff to maintain, just like adding more backends. Keep in mind that Idris2 is one of the possible frontends for the Core/TTImp language implemented in this repo and tooling would be very much tied to only the Idris2 frontend. Also while currently we are heavily in the unstable part of the language development, some time in the future, stability would mean that compiler release will require potentially a lot of time between one release to another, and I don't think tooling should be tied to the release constraint of the compiler.
That looks amazing! Maybe we should really start setting up a project to work on this. It might be a good candidate for a hackathon project!
Maybe off topic, but I'm wondering if we should make an Idris2-community Github group, so multiple people can accept PRs. We could do the LSP server, the Emacs mode, and any common libraries that are not quite main enough for contrib. It might take some of the traffic off of the main repo for e.g. PRs on contrib, and make less work for Edwin and Guillaume
@JoeyEremondi I am totally in for this. Besides, Edwin said that contrib has nearly reached the point where it is too hard to maintain and comprehend for the small group of people responsible for that. (Maybe just Edwin and Guillaume ?)
I just created it at https://github.com/idris-community
@JoeyEremondi how will we communicate? Just GitHub? Slack? Gitter? Or something else?
@michaelmesser Maybe a combination of Slack and GitHub, unless we find the need for more? That way the core people are still in the loop for some things on slack, and the rest people can opt in our out of on GitHub
@JoeyEremondi where is the Slack?
@michaelmesser #idris on fpchat-invite.herokuapp.com
Just to note that there was/is an https://github.com/idris-hackers where other libraries were developed, along with the current idris-mode. I did mention this on the slack but I have given up on that slack, so thought I would mention here.
We have now refactored the IDE protocol representation and its encoding/decoding into a separate protocols package.
If this Feature Request is still relevant, perhaps this refactoring makes it easier to change the concrete representation of the various commands. So if this RFC is still relevant, consider updating it taking the new IDE protocol design into account.