agda
Interest in deeper integration with Agda
I've recently been dissatisfied with the state of Agda's editor support, so experimented with implementing a language server for it (and a basic client VS Code extension for testing).
The agda-language-server currently:
- interacts with Agda through the same interface as
agda-mode(except for hover) - exposes its behavior (primarily) through a custom LSP method
- does not implement most standard LSP requests
- implements the standard LSP hover request, but in a heuristic and overly simplistic way
By contrast, my experiment:
- integrates more closely with Agda, manually invoking the type checker, inspecting its state, and performing folds over abstract syntax to extract semantic information
- exposes its behavior through standard LSP requests
- does not implement any of the functionality of
agda-mode - implements the following LSP requests:
- Go to Declaration/Definition/References
- Document Highlight (highlight occurrences of the symbol under the cursor)
- Document Symbols (VS Code outline, search symbols within file)
- Hover (shows type of top-level definitions; type of local variables needs changes to Agda)
- Completions (currently half-baked, but much more should be possible)
Following this experiment, I'd like to file a series of PRs to integrate this functionality alongside the existing agda-mode functionality. It would make the server more complex, but much richer. I wanted to discuss before filing PRs for such large changes. Is there interest in this sort of functionality and server architecture?
Yes, we do want to have deeper integration with standard LSP requests. Your PRs will be more than welcome!
@andy0130tw and I have been busy working on making ALS available on browsers, that's why there are no new features or functionalities regarding LSP or Agda in the recent months.
Thank you!
I'll try to make my PR compatible with the browser support. How exactly does it work? I have to trick the typechecker to avoid reading from the local filesystem and instead use the unsaved versions of files users are editing. I also need filesystem access for files the user hasn't opened, since LSP doesn't (seem to) have a mechanism to read such files. Do you have a systematic way to do this?
For example:
A.agda
module A where
open import B
g = f
B.agda
module B where
f = ...
If the user is editing A.agda, how does the typechecker access B.agda?
You have to access files via out-of-band messaging. If the server is a standalone executable, it means native filesystem operations. In VS Code, you should use the file system API to ensure compatibility on web extensions.
@nvarner I would love to use your experimental LSP, however I am having tons of issues getting it setup in both neovim and vscode (with your extension for vscode). How did you get it running in vscode? Is there an easy way for me to set this up in neovim?
@highjeans my LSP server communicates in a nonstandard way (it listens on port 4096 and waits for a client to connect). I'm not familiar with the neovim LSP client, but I'd guess that without modifications, it may be difficult.
What kind of errors are you seeing in VS Code? There are some known issues resulting from shortcut prototyping, but nothing I'm aware of that would prevent the server from initializing altogether.
@nvarner
Output is the following:
[Error - 3:17:29 PM] Client Language Server Example: connection to server is erroring.
Shutting down server.
[Error - 3:17:29 PM] Client Language Server Example: connection to server is erroring.
Shutting down server.
[Error - 3:17:29 PM] Stopping server failed
Error: Client is not running and can't be stopped. It's current state is: starting
at LanguageClient.shutdown (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/common/client.js:964:19)
at LanguageClient.stop (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/common/client.js:935:21)
at LanguageClient.stop (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/node/main.js:150:22)
at LanguageClient.handleConnectionError (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/common/client.js:1196:18)
at process.processTicksAndRejections (node:internal/process/task_queues:105:5)
[Error - 3:17:29 PM] Stopping server failed
Error: Client is not running and can't be stopped. It's current state is: starting
at LanguageClient.shutdown (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/common/client.js:964:19)
at LanguageClient.stop (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/common/client.js:935:21)
at LanguageClient.stop (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/node/main.js:150:22)
at LanguageClient.handleConnectionError (/Users/highjeans/.vscode/extensions/agda.agda-vscode-1.0.0/client/node_modules/vscode-languageclient/lib/common/client.js:1196:18)
at process.processTicksAndRejections (node:internal/process/task_queues:105:5)
[Info - 3:17:29 PM] Connection to server got closed. Server will restart.
true
[Error - 3:17:29 PM] Server initialization failed.
Message: Socket closed before the connection was established
Code: -32099
[Error - 3:17:29 PM] Language Server Example client: couldn't create connection to server.
Message: Socket closed before the connection was established
Code: -32099
[Error - 3:17:29 PM] Client Language Server Example: connection to server is erroring.
Cannot call write after a stream was destroyed
[Error - 3:17:29 PM] Server initialization failed.
Message: Cannot call write after a stream was destroyed
Code: -32099
[Error - 3:17:29 PM] Language Server Example client: couldn't create connection to server.
Message: Cannot call write after a stream was destroyed
Code: -32099
[Error - 3:17:29 PM] Restarting server failed
Message: Cannot call write after a stream was destroyed
Code: -32099