Update of extension

[racs4]

Hello, I tried to update the extension for the newest version of kind. My experience with lsp was none before i started this, so there is much more to do, and i appreciate some contribution/hints/critics/suggestions.

Some items of my contribution:

• I brought the kind lsp code to this repository. Before it was separated, I think because before it was impossible to run/check kind code outside the base folder.
• Added 3 tasks accessible via ctrl+ror cmd+r in vscode. They are:
  • kind-check: checks all the Lsp code
  • kind-check-clean: removes the cache and check
  • npm build: builds the kind.js file
• Isolated the process of checking the file. Now all that process is in src/Lsp/Check.kind and from there we can call the functions for on_change, on_hover, etc.
• Tried to optimize the process of change and hover. The isolated check returns two results: kind_defs and lsp_defs. The first one is a map of normal definitions described in Kind checking, and the second one is almost the same, but with an addition of a references map, that contains all references find while checking for one term. Then this can be used for hover and check at the same time.
• Tried to organize de lsp kind code and the lsp typescript code.
• Removed the initialized checking on the workspace. I did this because i constantly get stack overflow due to the big quantity of files being checked.

Things that need improvement:

• The check is slow sometimes (when there is no cache or the cache needs to change several times), and increases proportionally with the file size. The delay time of editing a file and getting a response is big.
• I didn't did anything about autocomplete/definition. The autocomplete works sometimes though.
• lsp_defs and kind_defs are almost the same, should we join that? But this may cause trouble in kind caching system.
• A progression bar or load indication would be nice to indicate that the lsp is checking the file.

[simonhorlick]

This is fantastic! Thank you for the PR! I have a lot of questions about this so please give me a couple of days to have a look and try it out.

[racs4]

Let me know if you have any questions or problems, i would try to help

[simonhorlick]

Should the kind code stay in this repository, or should we upstream it into the kind repo? It would be better to have it here, but the problem is when there's upstream changes to the typechecker we have to fix the code here. Ideally there would be a stable api that we could write the LSP against so that would be less of a problem.

The jump-to-definition seems to be using relative paths which don’t resolve any more, but I’m sure this is an easy fix.

One of the main reasons I haven’t been able to update the plugin so far is that the type checker blows the stack somewhere and I haven’t yet been able to track down where. It sounds like this is the same reason you disabled the initial checking. Does the LSP still know about definitions you haven't opened in the vscode workspace, or do you need to open them to get the type information?

[simonhorlick]

Ok, I see why the jump to definition isn't working now. It's because the definitions are not loaded from a file, it's from the internet (in Kind.Synth.get_kind_code). That's interesting..