does $/cancelRequst cancel workspace/symbol？

Stream: lean4

[Shanghe Chen]

Hi, I want to add the ability for fuzzy searching workspace symbols in IJ. On the client end, there seems to be no way to determine when an LSP request should be sent to the server. As a result, many workspace/symbol requests are sent as the user types. When the user types new characters, the client now tries to cancel the old request with $/cancelRequest. However, it seems the responses are quite slow in the client’s trace log(testing with v4.11 and Mathlib and MIL)

E89F6BFA-74E1-4EA5-A6FC-5EEB093602A8.jpg

Any ideas? I checked some code and am not sure if the previous workspace/symbol request can be interrupted if it is still being handled by $cancel/request.

[Marc Huisinga]

VS Code works around this to some degree by only requesting the symbols when the user has stopped typing for a bit, though you can obviously still spam the server with requests if you add another character just after that.

The performance of this request downstream of Mathlib is definitely pretty horrible and we don't really handle $/cancelRequest at the moment. I'll look into these at some point.

[Shanghe Chen]

Thanks for the information. Yeah some debouncing algorithms are nice work around. I will try them too