LSP support

[Z-snails]

Currently LSP expects a .ipkg file in a parent directory of the source code, however sirdi doesn't generate one, so lsp doesn't work

Here are some potential solutions I can think of:

• Generate a ipkg file
  • Clutters the project
  • Still has problems with where sirdi puts the ttc/ttm files
• Update idris2-lsp to support sirdi
  • More work?
  • Potentially requires updating 2 projects when changes are made
  • Could this be mitigated with clever design decisions?

[eayus]

As a short term solution, I made sirdi copy the ipkg it used to build the project back to the root directory (see src/Build.idr, in the build function). However it seems something change has broken this along the way and no-one has noticed, so I guess investigating that is the first priority.

I'm not sure what the long term solution is yet to be honest. I don't particularly like the idea of intertwining the lsp and package manager as it makes maintenance more complicated, but it does seem the most practical approach. As package managers get more stable, it may also be worth looking at revisitng what interface the Idris2 compiler itself provides, as I feel like ipkgs should probably be made redundant eventually.

[michaelmesser]

Does/will Sirdi provide an API that LSP could use or should LSP invoke Sirdi with system? It looks like Sirdi invokes Idris with system while LSP uses the Idris API so integration might not be straightforward. Do you plan on making a PR to LSP to add support for Sirdi or would you like someone more familiar with LSP to try implement it? The relevant part of idris2-lsp is here.

[eayus]

@michaelmesser I'm in the process of doing a refactor which will split Sirdi into a library API and command line application - once that is done, then it should be easy to modify LSP to call Sirdi. Once that is done I'm happy to have a go at modifying LSP to support it (or if someone else wants to, feel free). I'm sure if we run into any trouble I can ask on the discord for help from someone more familiar with the LSP. But I think it should be relatively straightforward as the code should be just a modification of the currently supported ipkg system.

[michaelmesser]

It might be necessary to modify the way jump to definition across packages works to support Sirdi, but I'm not sure. It would also be nice if the LSP could function in the file that the function is defined it. Currently it can't because of https://github.com/idris-lang/Idris2/issues/2216