You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
MikaelMayer opened this issue
Nov 24, 2023
· 0 comments
· Fixed by #4869
Labels
kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelmakes-mikael-gratefulThis issue, is fixed, would make Mikael Mayer grateful
[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
The text was updated successfully, but these errors were encountered:
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>
kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelmakes-mikael-gratefulThis issue, is fixed, would make Mikael Mayer grateful
Dafny version
latest-nightly
Code to produce this issue
I don't have code to reproduce this.
Command to run and resulting output
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
The text was updated successfully, but these errors were encountered: