LSP for K

[ehildenb]

Language Server Protocol (LSP) is defined here: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/

The features we want to implement with LSP are:

• Tab/token completion.
• Goto definition.
• Bad-parse underlining.

Here is an existing Python package for LSP: https://pygls.readthedocs.io/en/latest/

We should be able to instantiate this to tab/token completion directly, by reading in compiled.json and taking in all the tokens that should be considered for tab completion.

[radumereuta]

First version should take as input the compiled.json and try to implement Tab token completion.
Scan the definition, collect all the tokens and send them through the LSP

[radumereuta]

The features described here have been implemented and added to the K repo.
More features related to the Language Server have been added here: runtimeverification/k-editor-support#39