fix: Clear Diagnostics when file is closed

[lovettchris]

fix: LSP when file is closed clear any diagnostics so the "problems" list is cleared in VS code.

Note: if we want "project" level errors we should implement the full PublishDiagnostics LSP protocol, specifically the part about if a language has a project system (for example C#) diagnostics are not cleared when a file closes. When a project is opened all diagnostics for all files are recomputed (or read from a cache), etc. I think we should implement this for lean lake projects, but it's a much bigger change.

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[Vtec234]

My five cents: there are two unrelated changes here.

The change that clears diagnostics when the file worker exits seems for the better. Leftover diagnostics are often noisy and out-of-date. Indeed computing them for an entire Lake project as you write would be ideal, but short of that we should do the clearing.

On the other hand the information -> hint change is likely to be controversial (many users including myself are quite used to the info squiggles) — I am not sure it is the right move. I'd happily approve the PR if it were just the first of the two changes.

[lovettchris]

Ok, I split the more controversial change out to separate PR:
#1600

[Kha]

Should this be moved into the watchdog instead? Sending a response after receiving exit looks weird and may explain the supposed deadlocks in the tests.

[lovettchris]

I saw the "exit" event as an ideal place to do it, just before the process terminates it sends the message. I don't see why that would create a deadlock, at worst it would mean some test doesn't see the messages get cleared ? But it seemed very reliable in VS code when I was opening and closing files manually. I suppose I could design a torture test to see if I can force it to break...

[Vtec234]

Sending a response after receiving exit looks weird and may explain the supposed deadlocks in the tests.

Hm, I missed the test failures. @lovettchris could you try clearing the diagnostics in the watchdog after sending the exit notification to the worker? Perhaps in terminateFileWorker could work.

[lovettchris]

Hm, I missed the test failures. @lovettchris could you try clearing the diagnostics in the watchdog after sending the exit notification to the worker? Perhaps in terminateFileWorker could work.

I see, the problem was in the test harness run.lean where it was expecting a specific order of messages in response to shutdown, I fixed the hang by changing the order of these two lines in response to "shutdown":

      | Message.request id "shutdown" _ =>
        st.hOut.writeLspResponse ⟨id, Json.null⟩
        shutdown

so that the ResponseId is always sent first. The tests should pass now.

[Vtec234]

, I fixed the hang by changing the order of these two lines in response to "shutdown":

I am not sure this is the right thing to do here. Note that from the watchdog's perspective, sending a response to the shutdown request means "we are ready to exit (i.e. kill the process)". But we are not ready to exit before the shutdown function is done, because that function ensures that the worker state is cleaned up. So I think the two statements should stay in the order they are currently at.

[lovettchris]

I am not sure this is the right thing to do here. Note that from the watchdog's perspective, sending a response to the shutdown request means "we are ready to exit (i.e. kill the process)". But we are not ready to exit before the shutdown function is done, because that function ensures that the worker state is cleaned up. So I think the two statements should stay in the order they are currently at.

So it's not just an 'ack' that shutdown was received? I could fix it by changing the test to expect the new diagnostics message before the ack on the shutdown...

[lovettchris]

I pushed this change, so run.lean now loops until the shutdown response is found. Turns out some of the "server" tests also needed this so I moved the code to a new lean helper method named lspShutdown.

[Vtec234]

@lovettchris the changes to the tests look good. It is legitimate for the server to send more messages after receiving the shutdown request, so the simulated client should handle those.

On the other hand I am still not sure about the clearing of diagnostics after receiving exit in the worker. Is there any reason not to do it in the watchdog (e.g. in terminateFileWorker) before replying to shutdown like @Kha suggested?

[lovettchris]

On the other hand I am still not sure about the clearing of diagnostics after receiving exit in the worker. Is there any reason not to do it in the watchdog (e.g. in terminateFileWorker) before replying to shutdown like @Kha suggested?

Ok, I moved it.

[Vtec234]

Thanks, lgtm! We'll see in practice if all editors are happy with this change.

[lovettchris]

All tests are passing except on Linux Debug which got a very strange error:

[Kha]

Please revert the stray changes

[lovettchris]

Please revert the stray changes

Done.