Agda Support

[oati]

I don't exactly know what editor features helix would need for a complete agda experience. I'm hoping someone more experienced with agda could help with this.

Agda has an issue for LSP support: agda/agda#3758
There is an implementation: https://github.com/banacorn/agda-language-server

It seems like helix would need

• unicode input (although you could just use a compose key)
• support for holes
• special commands and messages (this would probably be more appropriate as a plugin, unless LSP supports language-specific custom commands)

I also don't know how much should be handled by the LSP server and not helix.

Possibly relevant: microsoft/language-server-protocol#1414

[pretentious7]

I'd started on this in a branch (only stubs im afraid) #3092

I'd be happy to collaborate, but I'm also an agda novice.

[blitzerr]

@pretentious7 thank you for doing this. Any further progress on this one ? I am unsure about how actively ASL is being developed. Is there any chance we can incorporate the Agda-mode like they have for emacs ?

[pretentious7]

I got a bit bamboozled by the als source (and agda in general...), I'll make another go of it in a couple months.

I'd like agda-mode type hole completion and stuff would be cool.

[omentic]

@pretentious7 Were you ever able to get als working?

I have pretty-good syntax highlighting working in #8285. I've been trying to get it to highlight function implementations to unfortunately no avail yet. The LSP has absolutely been mind-boggling though - I can't figure out what it's doing, let alone why it doesn't work - it seems to be failing to handle even basic file-was-saved events?

[pretentious7]

@pretentious7 Were you ever able to get als working?

I have pretty-good syntax highlighting working in #8285. I've been trying to get it to highlight function implementations to unfortunately no avail yet. The LSP has absolutely been mind-boggling though - I can't figure out what it's doing, let alone why it doesn't work - it seems to be failing to handle even basic file-was-saved events?

Same here... I switched to emacs about a year back, though, and agda-mode is fine for me.

[omentic]

Good to know 🙁 I have a sneaking suspicion that it relies on some emacs-specific implementation...

[omentic]

(the function highlighting issue turned out to be a bug in tree-sitter core. still have yet to figure out als)

[venus-as-a-boy]

Checking in to see if anyone has made progress on this. If not I might check out what vscode and emacs are doing and see if I can take a crack.

[omentic]

VSCode and Emacs rely on conventionalized extensions to the LSP protocol to communicate.

The Agda language server only supports type inference on hover (agda/agda-language-server#25) in the standard. Everything else is a custom method. This means this issue is pretty much blocked on #8675, because I doubt that the developers would want to support language-specific protocol extensions in core.

This is also blocked on having some sort of proof-general style interface. I think there could be a good pitch for including this in core, and it could probably reuse a lot of the debug interface. But it would be a lot of work and rely on implementing the protocol extensions.