Dafny server internal error

[tchajed]

Dafny version

4.2.0

Code to produce this issue

The error was transient while typing and immediately went away, so I'm not sure how you can reproduce it. I have the defaults set, to verify onchange and without caching.

Command to run and resulting output

No response

What happened?

The language server crashed with the following backtrace:

  Message: Internal Error - System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.LanguageServer.Workspace.NotificationPublisher.PublishGutterIcons(IdeState state, Boolean verificationStarted)
   at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.ResolveAsync()
   at Microsoft.Dafny.LanguageServer.Workspace.ProjectManager.GetSnapshotAfterResolutionAsync()
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyDocumentSymbolHandler.Handle(DocumentSymbolParams request, CancellationToken cancellationToken)
   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()
  Code: -32603 

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

Mac

[MikaelMayer]

I had a similar trace here recently

System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.AstExtensions.GetMemberQualification(MemberDecl memberDecl) in dafny\Source\DafnyCore\AST\IHasUsages.cs:line 31
   at Microsoft.Dafny.Method.GetQualifiedName() in dafny\Source\DafnyCore\AST\Members\Method.cs:line 384
   at Microsoft.Dafny.Method.GetDescription(DafnyOptions options) in dafny\Source\DafnyCore\AST\Members\Method.cs:line 375
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler.CreateSymbolMarkdown(ISymbol symbol) in dafny\Source\DafnyLanguageServer\Handlers\DafnyHoverHandler.cs:line 436
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler.GetStaticHoverContent(HoverParams request, IdeState state) in dafny\Source\DafnyLanguageServer\Handlers\DafnyHoverHandler.cs:line 82

[keyboardDrummer]

The first one will be a non-issue when the clients turns off gutter icon publishing on the server, which I think can happen soon.

The second seems unrelated to me, and not necessarily caused by a race condition. Is it not reproducible @MikaelMayer ?

[MikaelMayer]

I could not reproduce it, but if I can I'll open an issue.