FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Send response when lookup IDE request fails.

Open gebner opened this issue 1 year ago • 2 comments

The lookup request is the only one which does not return any response if the request failed. This makes it hard to support it in a generic API for IDE requests. See discussion at https://github.com/FStarLang/fstar-vscode-assistant/issues/27#issuecomment-1889687807

The history of the failure response for this request is interesting: it has flipped several times over the last year. I have summarized the responses for the different editors in the table below. I could not find any justification for the changes, the current vscode extension seems to work just fine with the change. This PR effectively reverts the behavior to how it was in 2022. 

time vscode emacs
2022 NOK NOK
after 754a6d8f1d2d5c6a0816bf24499a12896e0eb369 OK OK
after 6f979fb1dd53ada793682bd892473e78225fe05a nothing NOK
after this PR NOK NOK

gebner avatar Jan 12 '24 23:01 gebner

So apparently the lookup query is used internally by full-buffer.

gebner avatar Jan 13 '24 00:01 gebner

So apparently the lookup query is used internally by full-buffer.

I've added a new internal query type to ignore errors. The full-buffer command now uses this to suppress error messages when generating the internal lookup queries, while keeping the 2022 semantics of lookup. (Though I don't think the error messages broke anything except for the tests.)

gebner avatar Jan 16 '24 21:01 gebner

The vscode extension now avoids the awkward version of the lookup query, and no longer uses the internal lookup queries either.

The right choice is probably to just remove the internal lookup queries entirely.

gebner avatar Apr 26 '24 18:04 gebner