search

DafnyVSCode / Dafny-VSCode

Dafny 2 for Visual Studio Code (Legacy)
https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode-legacy
MIT License
18 stars 12 forks source link

Dafny extension does not work anymore - Request textDocument/codeAction failed. #84

Closed tflinkow closed 1 year ago

tflinkow commented 1 year ago

I had Dafny working in VS Code just fine for a long time. I have no idea what happened, but something happened while working on some Dafny files, causing the extension to not verify anything anymore. It just crashes with the following exception (even when creating a new file and just saving it as a .dfy file without content.

I tried reinstalling the extension multiple times and also removed VS Code completely and then reinstalled it and the extension again, but that does not help either (maybe there are still some leftover files anywhere?).

I'm on Windows 11.

[Error - 17:57:27] Request textDocument/codeAction failed.
  Message: Internal Error - System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.Resolver.SeqTypeArgToBeResolved.ToString()
   at Microsoft.Dafny.TypeConstraint.ErrorMsg.<Reporting>g__RemoveAmbiguity|5_0(Object[] msgArgs)
   at Microsoft.Dafny.TypeConstraint.ErrorMsg.Reporting(ErrorReporter reporter, String suffix)
   at Microsoft.Dafny.TypeConstraint.ReportErrors(ErrorReporter reporter)
   at Microsoft.Dafny.Resolver.SolveAllTypeConstraints()
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(TextDocumentItem document, Program program)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(TextDocumentItem textDocument, Program program, Boolean& canDoVerification, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(DocumentTextBuffer textDocument, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.<>c__DisplayClass12_0.<<LoadAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.Compilation.ResolveAsync()
   at Microsoft.Dafny.LanguageServer.Workspace.DocumentManager.GetLastDocumentAsync()
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.Handle(CodeActionParams 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
tflinkow commented 1 year ago

wrong repository, I apologise