Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support multiple ide server instances #2586

Merged
merged 3 commits into from
Jul 18, 2022

Conversation

dunhamsteve
Copy link
Contributor

The primary issue this addresses is that there can be only one ide server running at the same time, because they all use the same socket number. (idris-community/idris2-mode#26).

Since the plugins read the socket number from stdout, this could be worked around by opening socket "0" which means "choose an open socket", but idris2 currently prints the configured value rather than the actual socket number that was chosen by the OS.

This PR changes --ide-mode-socket to print the number of the socket that was opened, rather than the configured value. This change enables --ide-mode-socket :0 to work correctly.

It also changes the default socket to 0. This change allows existing clients to benefit from having more than one server running at a time, without change. But it assumes they respect the socket number printed on stdout. I don't see any evidence via google of anyone hardcoding the number 38398, so I think this is safe.

If clients do want a specific socket, they can still specify it on the command line.

Do any plugins besides the emacs ones use ide-mode-socket?

@dunhamsteve dunhamsteve changed the title Ide random socket Support multiple ide server instances Jul 13, 2022
@gallais
Copy link
Member

gallais commented Jul 14, 2022

This change allows existing clients to benefit from having more than one server running at a time, without change

🥰

But it assumes they respect the socket number printed on stdout. I don't see any evidence via google of anyone hardcoding the number 38398, so I think this is safe.

I think this is a perfectly fine to assume of modes. Can you please add this explicitly
to the documentation of the protocol?
This document aims to make easy to implement new clients without having to reverse
engineer the protocol.

Do any plugins besides the emacs ones use ide-mode-socket?

Edwin's vim mode I suspect? https://github.com/edwinb/idris2-vim

@mattpolzin
Copy link
Collaborator

Edwin's vim mode I suspect?

If I understand correctly, that Vim plugin actually uses Idris2 to execute 1-off commands via the --client flag; I’m not sure, but I believe that means it uses REPL supported syntax as opposed to the IDE protocol.

@dunhamsteve
Copy link
Contributor Author

Switching to ide mode doesn't seem to be mentioned at all in that document. I'll add a short section on how to put idris2 into both socket and non-socket ide mode. I think it should go at the top before "Protocol Overview", so it flows from how to initiate ide mode to how to talk to it.

@dunhamsteve
Copy link
Contributor Author

It looks like Sphinx needs a space between a colon and the trailing ::. Otherwise it renders :: in the output. I adjusted the rest of the file to fix this.

@gallais gallais added status: confirmed bug Something isn't working cli: ide-mode labels Jul 18, 2022
@gallais gallais merged commit c69af04 into idris-lang:main Jul 18, 2022
@dunhamsteve dunhamsteve deleted the ide-random-socket branch August 15, 2022 22:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants