Feature request: client-server configuration with Agda running elsewhere

[glangmead]

I'm imagining having Agda running on a server listening on a port (perhaps using your other project https://github.com/banacorn/agda-language-server) and VSCode running locally with the extension pointed at the server URL instead of a local path to the binary. Why? Probably many use cases, but in my world there are users who struggle to install Agda, who struggle to keep up with its versions, or whose hardware is not up to the RAM/CPU challenge of cabal install Agda but where VSCode runs smoothly. It would be good to delegate the Agda server to different experts and let the user be productive. Or in a classroom setting where the focus is on Agda and a local install per-student is not needed.

[banacorn]

This is definitely on the roadmap.
It's a nightmare to ask dozens of students to install Agda on their machine.

The good news is, it seems like users don't even have to install VS Code on their machine, a browser will do just fine.

@Zekt somehow managed to pulled this off and had a working agda-mode running in his browser when we were preparing for a summer school in Taiwan. Need more input from him.

[Zekt]

To run VS Code remotely is quite simple, you just need to install code server and Agda on a server, then you can access the VS Code and install agda-mode-vscode as usual.

I think it's currently not suitable for teaching though, because code-server does not support multiple users, which means there are no separated environments, you will need to ask each person to edit their own file only and do not interfere with others'. And type-checking will be quite slow, imagining type-checking 30 Agda files simultaneously on one machine.

I set a code-server up in case of someone not being able to install Agda on their machine, for small numbers (<5) of users it worked quite well.

It might be possible to run multiple instances of code-server and Agda with docker to solve above issues, but you probably need a strong server (one Agda instance can take a lot of memory).

[Zekt]

There is another way to achieve what @glangmead describes, one can run Agda on a server and others (supposedly students) can connect to that server using VS Code and agda-mode-vscode on their own machines.

You can bind an Agda server to a port using socat on the server:
socat -d -d TCP4-LISTEN:<port> EXEC:"<path to agda> --interaction"
And in the extension settings of the user's VS Code, set Agda Path to
socat - TCP4:<server ip>:<port>
agda-mode-vscode will then treat it as a local running Agda. You will need socat installed both on the server and local machines (nc works as well).

BUT, currently agda-mode-vscode will check if Agda exists by running what is in Agda Path before sending messages to it, I removed that part of code to make this work, would be nice if the check can be toggled off.
And there will probably be security concerns, better try it on a clean server and only run it on LAN with people you trust.

Edit: the set up process on the local machine is incorrect as I forget how I did it, will update.

[glangmead]

Thanks @Zekt, that's promising! code-server is cool but I also discovered some of the drawbacks you mentioned. It also seemed like learning to use a service to serve docker images is easier than learning to use a service that serves docker images and offers persistent storage for all the data, and so my mind gradually moved to the model where the Agda server is stateless and the user deals with git and their source files plus VSCode on their end. I look forward to trying your socat setup at some point.

[jespercockx]

@Zekt I tried to run this plugin from code-server as you described, I got code-server to run however I'm not able to install the plugin as you describe. It seems that code-server does not have access to the extensions on the VS marketplace (see https://github.com/cdr/code-server/blob/c4610f7829701aadb045d450013b84491c30580d/doc/FAQ.md#differences-compared-to-vs-code), and instead runs its own marketplace with only open-source addons which it scrapes from github. Should I make an issue there to add the addon or is there something that can be done on this side so it is picked up automatically?

[glangmead]

@jespercockx I submitted coder/code-server#2177 a few months ago for the same reason. You probably know this but you can go still install the extension by hand by going to https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode and download the extension (it ends in .vsix), then in VSCode go to Extensions, click the "..." dots icon then "Install from VSIX..." and browse to the file

[jespercockx]

Ah I see, so there is already an issue for that. I managed to work around the problem by copying my local .vscode configuration to the code-server installation, but it's good to know that there's also a direct way to do it. Thanks!