ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

Accumulated performance stats on selection hover #690

Open Alizter opened 4 months ago

Alizter commented 4 months ago

I'm not fully certain how this would work for other performance stats but for time we could imagine a feature where the user selects a range and then hovers over it. This would then display the total execution time for the block.

That could be useful for analysing proof scripts where line-by-line performance might be uninformative but a collective total might give more insight.

ejgallego commented 4 months ago

That'd be indeed cool to have!

One problem is that hover doesn't transmit selection data to the server, so that would require an extension to the standard with either a new request or an extra parameter to hover.

This is issue https://github.com/microsoft/language-server-protocol/issues/377

But indeed, we could implement this on our side, usually an update to the protocol requires several extensions implement the proposal, so indeed, green light from me to support extended hover.

The way to do this is:

ejgallego commented 4 months ago

See this code in hover.ts:

    protected registerLanguageProvider(options: HoverRegistrationOptions): [Disposable, HoverProvider] {
        const selector = options.documentSelector!;
        const provider: HoverProvider = {
            provideHover: (document, position, token) => {
                const client = this._client;
                const provideHover: ProvideHoverSignature = (document, position, token) => {
                    return client.sendRequest(HoverRequest.type, client.code2ProtocolConverter.asTextDocumentPositionParams(document, position), token).then((result) => {
                        if (token.isCancellationRequested) {
                            return null;
                        }
                        return client.protocol2CodeConverter.asHover(result);
                    }, (error) => {
                        return client.handleFailedRequest(HoverRequest.type, token, error, null);
                    });
                };
                const middleware = client.middleware;
                return middleware.provideHover
                    ? middleware.provideHover(document, position, token, provideHover)
                    : provideHover(document, position, token);
            }
        };
        return [this.registerProvider(selector, provider), provider];

So indeed you want the middleware to fully handle the request in this case and add the extra parameter.

Alizter commented 4 months ago

It seems rust-analyzer has an implementation of this:

https://github.com/microsoft/language-server-protocol/issues/377#issuecomment-889898650

ejgallego commented 4 months ago

It seems rust-analyzer has an implementation of this:

microsoft/language-server-protocol#377 (comment)

Yes, tho I would not use their choice for overloading position; I guess they do different these days.

Alizter commented 4 months ago

Yes, that doesn't seem like a good choice. The better option is to have an optional range field in addition as discussed in the thread.

ejgallego commented 4 months ago

They still do the same: https://github.com/rust-lang/rust-analyzer/blob/25f59be62f6b915b44a4c2ec2defca56a5f766c1/editors/code/src/client.ts#L228

The use exactly the implementation I suggested, the new middleware support is superb !