-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: Added code to catch resolver exceptions if any. #2080
Conversation
Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs
Outdated
Show resolved
Hide resolved
visitor.Visit(symbolTable.CompilationUnit.Program); | ||
return visitor.GhostDiagnostics; | ||
} catch (Exception e) { | ||
logger.LogDebug(e, "encountered an exception while getting ghost state diagnostics of {Name}", symbolTable.CompilationUnit.Name); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This will not be visible to users, right? Aren't these logs only written to disk in a somewhat hidden location?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes they are written next to DafnyLanguageServer.dll, and only if an option is activated.
But this kind of error can happen if the language server recovered from problematic resolving, and leaving the program in a state that the Ghost Diagnostic Collector is not assuming, so that's why it's less important.
…olver.cs Co-authored-by: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com>
Can we add tests by using dependency injection to inject a broken implementation? The reason I ask is because having a reliable language server is so important and without tests it seems easy to lose the functionality you added in this PR again. |
Yes you're right. |
|
||
[TestMethod] | ||
public void EnsureResilienceAgainstErrors() { | ||
// Builtins is null to trigger an error. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It seems like this test relies on some badly defined API of DafnyPipeline.csproj
, that it requires Builtins to be not null, to trigger the exception. I think it might be nicer if the test uses a more explicit API to trigger a failure, like mocking something from DafnyPipeline.csproj
and letting the mock throw an Exception, but I imagine DafnyPipeline.csproj
is not setup for being mocked.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes you identified this test correctly.
I don't see either how to mock the DafnyPipeline, so I took the route of the minimum working test for now.
As a prevention measure for issues such as #2074
I added some code that catches exceptions coming from the Resolver so that it won't impact user experience in the IDE.
I also added some catching code for Ghost Diagnostics because they were impacted as well.
The result is a non-blocking diagnostic that does not crash the server anymore:
Moreover, it returns also all the other resolution errors so that users are not helpless:
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.