Is inlay hints implemented or planning in the lsp server

Stream: lean4

[Shanghe Chen]

Hi @Manu Bhat and I may be interested in displaying some infos or goals inline an editor in Intellij Idea or RustRover. Investing this it seems requiring the lsp server support Inlay Hints Is it implemented or any plan for it?

[Marc Huisinga]

Not in the near future.

There are several problems with inlay hints that mean that we won't implement them soon:

• Their cursor behavior in VS Code is very broken, so they would be annoying to most users and disabled by default
• We'd really like to report inlay hints as the file is being processed, which is currently not possible because VS Code does not support LSP's partial results, so the latency until they show up can be very large (I may be able to solve this one in the future)
• We'd somehow need to mitigate the issue of inlay hint flickering, which is difficult to do nicely because LSP doesn't tell us where the text cursor is
• They need to be compatible with whatever we decide on for a formatter in the future

[Shanghe Chen]

Got it. Thanks for the comprehensive information!