You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A name conflict between the lsp package (lsp) and coq-lsp.lsp makes it impossible to use them both together due to a module name clash. Both libraries export a module named Lsp.
To Reproduce
In a Dune project, try linking lsp and coq-lsp.lsp
Thanks for the report, will fix ASAP by renaming the module to Fleche_lsp.
We'd like to use upstream LSP libraries (cc: #2 ), however, we support some extensions, for example with Range-based offsets, which make us hard to use them for now.
But it is still in the roadmap to eventually remove our own Lsp implementation.
Describe the bug
A name conflict between the lsp package (lsp) and coq-lsp.lsp makes it impossible to use them both together due to a module name clash. Both libraries export a module named Lsp.
To Reproduce
In a Dune project, try linking lsp and coq-lsp.lsp
Dune will indicate various errors when trying to use anything from Lsp
Expected behavior
As both libraries can be used together, renaming the
coq-lsp.lsp
module to something more precise would avoid the name conflict.Desktop
Additional context
The text was updated successfully, but these errors were encountered: