[lsp] Support incremental checking

[ejgallego]

The current server doesn't support incremental checking. [We had a branch but it didn't survive]

I suggest we implement prefix-only incremental checking; in order to do this two orthogonal changes are necessary:

• improve protocol support so IDEs can send changes incrementally. This requires add some text-processing system and refactoring of the server code.
• compute a common prefix for checking; we could also send diagnostics more often as to improve reactivity.

[ejgallego]

By the way this is still on the plan, however we are discussing some stuff about sharing lsp infrastructure with other ocaml tooling.

[amelieled]

Just for your information, a file with almost 1 000 lines, isn't check quickly.
It's really a problem.

[ejgallego]

Indeed @amelieled ; it would be easy to give prefix-only checking a go; basically:

• parse the new document
• compute the common prefix
• check from there

I am away from home since Feb and I've been having terrible bureaucratic problems due to the ongoing global pandemic, but I expect to return to France this saturday, that should improve my situation a lot so I could help with implementing that if you feel like doing it together.

For the medium term, I'm still working on the right strategy for incremental checking that hopefully can be shared among dedukti / Coq; it is a tad more complex as it is based on real-world incremental computing engines, so you basically maintain a DAG where edges are build / check rules. That provides really good performance, however the simpler prefix trick should much improve your problem.

[fblanqui]

Hi @ejgallego ! It's good to hear from you. I hope every thing will be all right for you. For your information, Amélie started a M2 internship about one month ago. She's going to work on induction in LP. If she wants to contribute to the development of prefix-only checking, why not, but this should not take her too much time as this is not the main objective of her internship.

[ejgallego]

Hi @fblanqui ; indeed I'll try to do something quick next week so Amélie can test; I agree she should not be distracted from her main goal. I'd be happy to answer any questions she may have about that part of the code in case she feels curious.

[amelieled]

Hi! I agree with you as well. But I'm also interested in learning, and perhaps helping, on this subject. Feel free to let me know what I can read/work to help you. I'm still far from knowing all the code to this git!