Document Lean's Language Server Functionalities

[Julian]

What question should the reference manual answer?: The language server protocol is language-agnostic of course, which means each language gets to in some way "plug in" to the hooks that are offered. This means in particular that it's useful to know what functionality is implemented by a language server, and how it relates to the language. In particular, a specific question might be "what semantic tokens are sent back by the semantic highlighting support in Lean, and how do they relate to Lean's syntax categories".

Please describe what the reference manual should enable you to do that you can't do right now

Here are some sample questions that might be useful to answer (though maybe the "how" is more suited for tutorials and just the "which" are suitable for here...):

• of the non-"universal" LSP methods, which additional optional ones does the LS implement in Lean?
• How does completion work (which responses are returned), how does semantic highlighting work (which tokens are emitted)
• What code actions are defined, and how are new ones registered?
• what is Lean's RPC framework, and what additional functionality does it layer on? What API exists for adding or interacting with RPC methods?

Additional context
Some prior art is already in the docs clearly. E.g. https://lean-lang.org/lean4/doc/semantic_highlighting.html?highlight=semantic#semantic-highlighting exists for some of the semantic highlighting questions above

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Discussion.20thread.20for.20Lean.20Language.20Reference/near/494413278

[david-christiansen]

These are important topics!

They're much lower priority than other topics right now, so it will be some time before this is written, if ever.