Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Dafny Language Server crashing occasionally #4818

Closed
MikaelMayer opened this issue Nov 24, 2023 · 0 comments · Fixed by #4869
Closed

Dafny Language Server crashing occasionally #4818

MikaelMayer opened this issue Nov 24, 2023 · 0 comments · Fixed by #4869
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

I don't have code to reproduce this.

Command to run and resulting output

[Trace - 1:21:41 PM] Received response 'textDocument/codeAction - (181)' in 38ms. Request failed: Internal Error - System.InvalidOperationException: Sequence contains no matching element
   at System.Linq.ThrowHelper.ThrowNoMatchException()
   at System.Linq.Enumerable.First[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.LanguageServer.ErrorMessageDafnyCodeActionProvider.FindTokenRangeFromLspRange(IDafnyCodeActionInput input, Range range) in dafny\Source\DafnyLanguageServer\Language\ErrorMessageDafnyCodeActionProvider.cs:line 32
   at Microsoft.Dafny.LanguageServer.ErrorMessageDafnyCodeActionProvider.GetDafnyCodeActions(IDafnyCodeActionInput input, Diagnostic diagnostic, Range selection) in dafny\Source\DafnyLanguageServer\Language\ErrorMessageDafnyCodeActionProvider.cs:line 20
   at Microsoft.Dafny.LanguageServer.Plugins.DiagnosticDafnyCodeActionProvider.GetDafnyCodeActions(IDafnyCodeActionInput input, Range selection) in dafny\Source\DafnyLanguageServer\Plugins\DafnyCodeActionProvider.cs:line 59
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.<>c__DisplayClass6_0.<GetFixesWithIds>b__0(DafnyCodeActionProvider fixer) in dafny\Source\DafnyLanguageServer\Handlers\DafnyCodeActionHandler.cs:line 53
   at System.Linq.Enumerable.SelectManySingleSelectorIterator`2.ToArray()
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.Handle(CodeActionParams request, CancellationToken cancellationToken) in dafny\Source\DafnyLanguageServer\Handlers\DafnyCodeActionHandler.cs:line 73
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.<RouteRequest>g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(IRequestDescriptor`1 descriptors, Request request, CancellationToken token)
   at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__DisplayClass10_0.<<RouteRequest>b__5>d.MoveNext() (-32603).
[Error - 1:21:41 PM] Request textDocument/codeAction failed.
  Message: Internal Error - System.InvalidOperationException: Sequence contains no matching element
   at System.Linq.ThrowHelper.ThrowNoMatchException()
   at System.Linq.Enumerable.First[TSource](IEnumerable`1 source, Func`2 predicate)
   at Microsoft.Dafny.LanguageServer.ErrorMessageDafnyCodeActionProvider.FindTokenRangeFromLspRange(IDafnyCodeActionInput input, Range range) in dafny\Source\DafnyLanguageServer\Language\ErrorMessageDafnyCodeActionProvider.cs:line 32
   at Microsoft.Dafny.LanguageServer.ErrorMessageDafnyCodeActionProvider.GetDafnyCodeActions(IDafnyCodeActionInput input, Diagnostic diagnostic, Range selection) in dafny\Source\DafnyLanguageServer\Language\ErrorMessageDafnyCodeActionProvider.cs:line 20
   at Microsoft.Dafny.LanguageServer.Plugins.DiagnosticDafnyCodeActionProvider.GetDafnyCodeActions(IDafnyCodeActionInput input, Range selection) in dafny\Source\DafnyLanguageServer\Plugins\DafnyCodeActionProvider.cs:line 59
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.<>c__DisplayClass6_0.<GetFixesWithIds>b__0(DafnyCodeActionProvider fixer) in dafny\Source\DafnyLanguageServer\Handlers\DafnyCodeActionHandler.cs:line 53
   at System.Linq.Enumerable.SelectManySingleSelectorIterator`2.ToArray()
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.Handle(CodeActionParams request, CancellationToken cancellationToken) in dafny\Source\DafnyLanguageServer\Handlers\DafnyCodeActionHandler.cs:line 73

What happened?

I should not get issues, but I occasionally get these issues.

What type of operating system are you experiencing the problem on?

Windows
@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful labels Nov 24, 2023
@keyboardDrummer keyboardDrummer mentioned this issue Dec 12, 2023
Merged
keyboardDrummer added a commit that referenced this issue Feb 9, 2024
@keyboardDrummer
Log an error instead of crashing in FindTokenRangeFromLspRange (#4869)
29c4525 
Fixes #4818

### How has this been tested?
Not. There's no known reproduction for the issue. This change uses
defensive coding to reduce the chance of a crash

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Log an error instead of crashing in FindTokenRangeFromLspRange keyboardDrummer/dafny
1 participant
@MikaelMayer