Currently, we supply build our own LSP client, and we start our own LSP server.
This has the advantage that we are in control, but also means we are maintaining a chunk of code that does some stuff, and means that we are conflicting with the main language plugins, which means we disable the other extensions.
In addition, the installation instructions for Lean involve installing the plugin anyway, which leads to the weird situation that we install the plugin just to immediately disable it. This might also cause confusion for users who already have lean installed and suddenly find their plugin disabled.
Investigate refactoring our code such that we can co-exist and make use of the Lean 4 extension and the Rocq-lsp extension.
- What would be the rough technical effort involved?
- What would be the integration point? Are the APIs of the language extensions enough for us?
- Can we prevent doubling of error messages and such?
Currently, we supply build our own LSP client, and we start our own LSP server.
This has the advantage that we are in control, but also means we are maintaining a chunk of code that does some stuff, and means that we are conflicting with the main language plugins, which means we disable the other extensions.
In addition, the installation instructions for Lean involve installing the plugin anyway, which leads to the weird situation that we install the plugin just to immediately disable it. This might also cause confusion for users who already have lean installed and suddenly find their plugin disabled.
Investigate refactoring our code such that we can co-exist and make use of the Lean 4 extension and the Rocq-lsp extension.