-
Notifications
You must be signed in to change notification settings - Fork 12
Description
This has happened multiple times, with no apparent cause since it happens as I am modifying code. It has happened with automatic verification onchange and onsave.
Note that I have redacted the path when copying the error message to here, but it is to a different .dfy file in the same folder as the file I was working on.
[Error - 12:23:00 PM] Request textDocument/codeAction failed.
Message: Internal Error - System.UnauthorizedAccessException: Access to the path [redacted] is denied.
at Microsoft.Win32.SafeHandles.SafeFileHandle.CreateFile(String fullPath, FileMode mode, FileAccess access, FileShare share, FileOptions options)
at Microsoft.Win32.SafeHandles.SafeFileHandle.Open(String fullPath, FileMode mode, FileAccess access, FileShare share, FileOptions options, Int64 preallocationSize)
at System.IO.Strategies.OSFileStreamStrategy..ctor(String path, FileMode mode, FileAccess access, FileShare share, FileOptions options, Int64 preallocationSize)
at Microsoft.Dafny.LanguageServer.Workspace.LanguageServerFilesystem.ReadFile(Uri uri)
at Microsoft.Dafny.ProgramParser.IncludeToDafnyFile(SystemModuleManager systemModuleManager, ErrorReporter errorReporter, Include include)
at Microsoft.Dafny.ProgramParser.TryParseIncludes(IReadOnlyList1 files, IEnumerable1 roots, SystemModuleManager systemModuleManager, ErrorReporter errorReporter, CancellationToken cancellationToken)
at Microsoft.Dafny.ProgramParser.ParseFiles(String programName, IReadOnlyList1 files, ErrorReporter errorReporter, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.DafnyLangParser.Parse(TextDocumentIdentifier document, ErrorReporter reporter, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(DafnyOptions options, VersionedTextDocumentIdentifier documentIdentifier, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.<>c__DisplayClass9_0.<<LoadAsync>b__0>d.MoveNext() --- End of stack trace from previous location --- at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadAsync(DafnyOptions options, VersionedTextDocumentIdentifier documentIdentifier, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.ResolveAsync() at Microsoft.Dafny.LanguageServer.Workspace.ProjectManager.GetLastDocumentAsync() at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.Handle(CodeActionParams request, CancellationToken cancellationToken) at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at MediatR.Pipeline.RequestPreProcessorBehavior2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at MediatR.Pipeline.RequestPostProcessorBehavior2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at MediatR.Pipeline.RequestExceptionProcessorBehavior2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at MediatR.Pipeline.RequestExceptionProcessorBehavior2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at MediatR.Pipeline.RequestExceptionActionProcessorBehavior2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at MediatR.Pipeline.RequestExceptionActionProcessorBehavior2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate1 next) at OmniSharp.Extensions.JsonRpc.RequestRouterBase1.g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase1.RouteRequest(IRequestDescriptor1 descriptors, Request request, CancellationToken token)
at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__DisplayClass10_0.<b__5>d.MoveNext()
Code: -32603