From 3b876aa40ae99c849c31d6573401decb58b652f1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 25 Jul 2023 01:11:21 +0200 Subject: [PATCH] Various fixes for project aware mode (#4299) Depends on https://github.com/dafny-lang/dafny/pull/4273 ### Changes 1. Take URIs into account when handling manual verification run and cancellation requests 1. Enable project aware mode option 1. Send compilation status updates for all documents owned by a project 1. Do not retrigger compilation of a project when opening an unchanged document of that project ### Tests 1. Add test `RunWithMultipleSimilarDocuments` 1. No test needed 1. Add test `CompilationStatusNotificationTest.MultipleDocuments` 1. Performance, difficult to test without an existing framework 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). --- .../AST/Grammar/CustomDirectoryInfoWrapper.cs | 3 +- .../ProjectFiles/CompetingProjectFilesTest.cs | 24 ++++-- .../ProjectFiles/MultipleFilesTest.cs | 12 ++- .../ProjectFiles/ProjectFilesTest.cs | 13 ++- .../Synchronization/CloseDocumentTest.cs | 2 +- .../DeclarationLocationMigrationTest.cs | 30 +++---- .../Synchronization/IncludeFileTest.cs | 3 +- .../Synchronization/LookupMigrationTest.cs | 18 ++--- .../Synchronization/OpenDocumentTest.cs | 17 ++-- .../Synchronization/SymbolMigrationTest.cs | 8 +- ...ationOrder.cs => VerificationOrderTest.cs} | 4 +- .../Synchronization/VerificationStatusTest.cs | 25 ++++++ .../Unit/CompilationManagerTest.cs | 3 +- .../Unit/TextDocumentLoaderTest.cs | 6 +- .../Util/ClientBasedLanguageServerTest.cs | 10 ++- .../Util/FileTestExtensions.cs | 32 ++++++++ .../CompilationStatusNotificationTest.cs | 58 +++++++++----- .../Various/ExceptionTests.cs | 4 +- .../Various/StabilityTest.cs | 6 +- .../Handlers/Custom/VerificationHandler.cs | 14 ++-- .../Handlers/DafnyCompletionHandler.cs | 2 +- .../Handlers/DafnyDefinitionHandler.cs | 2 +- .../Handlers/DafnyDocumentSymbolHandler.cs | 2 +- .../Handlers/DafnyHoverHandler.cs | 2 +- .../Handlers/DafnySignatureHelpHandler.cs | 2 +- .../Language/DafnyLangParser.cs | 8 +- .../Language/IDafnyParser.cs | 2 +- .../Language/LanguageServerExtensions.cs | 4 +- Source/DafnyLanguageServer/ServerCommand.cs | 4 +- .../Workspace/CompilationManager.cs | 2 +- .../CompilationStatusNotificationPublisher.cs | 29 ++++--- .../Workspace/Documents/Compilation.cs | 4 +- .../Documents/CompilationAfterParsing.cs | 2 +- ...ICompilationStatusNotificationPublisher.cs | 5 +- .../Workspace/IProjectDatabase.cs | 4 +- .../Workspace/ITextDocumentLoader.cs | 4 +- .../Workspace/IdeStateObserver.cs | 14 ++-- .../Workspace/LanguageServerExtensions.cs | 1 + .../Workspace/LanguageServerFilesystem.cs | 12 ++- .../Workspace/NotificationPublisher.cs | 80 +++++++++---------- .../Notifications/CompilationStatus.cs | 2 +- .../Workspace/ProjectManager.cs | 29 ++++--- .../Workspace/ProjectManagerDatabase.cs | 51 ++++++++---- .../Workspace/TextDocumentLoader.cs | 22 ++--- 44 files changed, 369 insertions(+), 212 deletions(-) rename Source/DafnyLanguageServer.Test/Synchronization/{VerificationOrder.cs => VerificationOrderTest.cs} (91%) create mode 100644 Source/DafnyLanguageServer.Test/Util/FileTestExtensions.cs diff --git a/Source/DafnyCore/AST/Grammar/CustomDirectoryInfoWrapper.cs b/Source/DafnyCore/AST/Grammar/CustomDirectoryInfoWrapper.cs index 582f7b43f6b..8aa4a0af412 100644 --- a/Source/DafnyCore/AST/Grammar/CustomDirectoryInfoWrapper.cs +++ b/Source/DafnyCore/AST/Grammar/CustomDirectoryInfoWrapper.cs @@ -1,6 +1,7 @@ // Licensed to the .NET Foundation under one or more agreements. // The .NET Foundation licenses this file to you under the MIT license. +#nullable enable using System; using System.Collections.Generic; using System.IO; @@ -59,7 +60,7 @@ public override IEnumerable EnumerateFileSystemInfos() { /// /// The directory name /// The directory - public override DirectoryInfoBase GetDirectory(string name) { + public override DirectoryInfoBase? GetDirectory(string name) { bool isParentPath = string.Equals(name, "..", StringComparison.Ordinal); if (isParentPath) { diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs index 7a200d45d54..2036af3fa26 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs @@ -1,22 +1,31 @@ +using System; using System.IO; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace; -using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; using Xunit.Abstractions; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles; public class CompetingProjectFilesTest : ClientBasedLanguageServerTest { + protected override Task SetUp(Action modifyOptions) { + return base.SetUp(o => { + o.Set(ServerCommand.ProjectMode, true); + modifyOptions?.Invoke(o); + }); + } + + /// /// A project should only publish diagnostics for uris which it owns, /// We can have a function filterOwnership(IdeState -> IdeState) /// that adds the "an error occurred outside this project" /// - [Fact(Skip = "Not yet supported")] + [Fact] public async Task ProjectFileDoesNotOwnAllSourceFilesItUses() { var tempDirectory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); var nestedDirectory = Path.Combine(tempDirectory, "nested"); @@ -24,12 +33,11 @@ public async Task ProjectFileDoesNotOwnAllSourceFilesItUses() { await File.WriteAllTextAsync(Path.Combine(nestedDirectory, "source.dfy"), "hasErrorInSyntax"); await File.WriteAllTextAsync(Path.Combine(nestedDirectory, DafnyProject.FileName), ""); - var outerProject = CreateTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName)); - await client.OpenDocumentAndWaitAsync(outerProject, CancellationToken); + await CreateAndOpenTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName)); - var diagnostics = await GetLastDiagnostics(outerProject, CancellationToken); + var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Single(diagnostics); - Assert.Contains("something about a file not owned by the project", diagnostics[0].Message); + Assert.Contains("the referenced file", diagnostics[0].Message); } public readonly string hasShadowingSource = @" @@ -44,7 +52,7 @@ method Foo() { /// Here the outer project loses ownership of this document. /// At this point we simply need to apply the filterOwnership function on its last published IdeState again /// - [Fact(Skip = "Not yet supported")] + [Fact] public async Task NewProjectFileGrabsSourceFileOwnership() { var tempDirectory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); var nestedDirectory = Path.Combine(tempDirectory, "nested"); @@ -66,6 +74,8 @@ public async Task NewProjectFileGrabsSourceFileOwnership() { Assert.Contains("Shadowed", diagnostics0[0].Message); await File.WriteAllTextAsync(Path.Combine(nestedDirectory, DafnyProject.FileName), ""); + await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime); + ApplyChange(ref sourceFile, new Range(0, 0, 0, 0), "//comment\n"); var diagnostics1 = await GetLastDiagnostics(sourceFile, CancellationToken); Assert.Empty(diagnostics1); diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesTest.cs index 595ac9204c0..cda4d9d3f0e 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesTest.cs @@ -176,7 +176,8 @@ method Produces() {} var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); Directory.CreateDirectory(directory); - await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource); + var projectFilePath = Path.Combine(directory, DafnyProject.FileName); + await File.WriteAllTextAsync(projectFilePath, projectFileSource); var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "firstFile.dfy")); var secondFile = await CreateAndOpenTestDocument(producer, Path.Combine(directory, "secondFile.dfy")); @@ -184,10 +185,7 @@ method Produces() {} var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3)); Assert.Empty(producesDefinition1); - // Wait to prevent an IOException because the file is already in use. - await Task.Delay(100); - await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), - @"includes = [""firstFile.dfy"", ""secondFile.dfy""]"); + await FileTestExtensions.WriteWhenUnlocked(projectFilePath, @"includes = [""firstFile.dfy"", ""secondFile.dfy""]"); await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime); var producesDefinition2 = await RequestDefinition(consumer, new Position(1, 3)); @@ -215,7 +213,7 @@ method Foo() { [options] warn-shadowing = true -"; // includes must come before [options], even if there is a blank line +".Trim(); // includes must come before [options], even if there is a blank line var directory = Path.GetRandomFileName(); var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName)); var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "src/file.dfy")); @@ -225,7 +223,7 @@ method Foo() { Assert.Contains(diagnostics1, s => s.Message.Contains("Shadowed")); await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime); - ApplyChange(ref projectFile, new Range(1, 17, 1, 21), "false"); + ApplyChange(ref projectFile, new Range(3, 17, 3, 21), "false"); var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextWarningOrErrorDiagnosticsAsync(CancellationToken); // The shadowed warning is no longer produced, and the verification error is not migrated. diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 8a280f32b10..02a63df942b 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -11,6 +11,13 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest; public class ProjectFilesTest : ClientBasedLanguageServerTest { + [Fact] + public async Task ProjectFileByItselfHasNoDiagnostics() { + var tempDirectory = Path.GetRandomFileName(); + await CreateAndOpenTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName)); + await AssertNoDiagnosticsAreComing(CancellationToken); + } + [Fact] public async Task ProjectFileChangesArePickedUpAfterCacheExpiration() { await SetUp(options => options.WarnShadowing = false); @@ -29,13 +36,13 @@ method Foo() { "; var documentItem = CreateTestDocument(source, Path.Combine(tempDirectory, "source.dfy")); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + await AssertNoDiagnosticsAreComing(CancellationToken); var warnShadowingOn = @" [options] warn-shadowing = true"; - // Wait to prevent an IOException because the file is already in use. - await Task.Delay(100); - await File.WriteAllTextAsync(projectFilePath, warnShadowingOn); + + await FileTestExtensions.WriteWhenUnlocked(projectFilePath, warnShadowingOn); await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime); ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "//touch comment\n"); var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs index 38254b6b723..2760f8a07ed 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs @@ -46,7 +46,7 @@ function GetConstant(): int { }".Trim(); var documentItem = CreateTestDocument(source); client.CloseDocument(documentItem); - Assert.Null(await Projects.GetResolvedDocumentAsync(documentItem.Uri)); + Assert.Null(await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri)); } public CloseDocumentTest(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs index c0cf806a056..8bdb46ff98a 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs @@ -52,7 +52,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((3, 0), (4, 1)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location)); Assert.Equal(new Range((0, 6), (0, 7)), location.Name); @@ -79,7 +79,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((3, 0), (4, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location)); Assert.Equal(new Range((0, 6), (0, 7)), location.Name); @@ -112,7 +112,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((3, 0), (4, 1)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "C", out var location)); Assert.Equal(new Range((10, 6), (10, 7)), location.Name); @@ -139,7 +139,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((3, 0), (4, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "C", out var location)); Assert.Equal(new Range((5, 6), (5, 7)), location.Name); @@ -166,7 +166,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((3, 19), (3, 22)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "GetX", out var location)); Assert.Equal(new Range((3, 11), (3, 15)), location.Name); @@ -190,7 +190,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((1, 2), (1, 13)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location)); Assert.Equal(new Range((0, 6), (0, 7)), location.Name); @@ -208,7 +208,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((0, 10), (0, 21)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location)); Assert.Equal(new Range((0, 6), (0, 7)), location.Name); @@ -232,7 +232,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((1, 2), (1, 13)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.False(TryFindSymbolDeclarationByName(document, "x", out var _)); } @@ -264,7 +264,7 @@ var a }".TrimStart() } ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "B", out var bLocation)); Assert.Equal(new Range((4, 6), (4, 7)), bLocation.Name); @@ -280,14 +280,14 @@ public async Task PassingANullChangeRangeClearsSymbolsTable() { var documentItem = CreateTestDocument(source); await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var state = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(state); Assert.True(TryFindSymbolDeclarationByName(state, "X", out var _)); // First try a change that doesn't break resolution. // In this case all information is recomputed and no relocation happens. await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "class Y {}"); - state = await Projects.GetResolvedDocumentAsync(documentItem); + state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem); Assert.NotNull(state); // No relocation, since no resolution errors, so Y can be found Assert.False(TryFindSymbolDeclarationByName(state, "X", out var _)); Assert.True(TryFindSymbolDeclarationByName(state, "Y", out var _)); @@ -295,7 +295,7 @@ public async Task PassingANullChangeRangeClearsSymbolsTable() { // Next try a change that breaks resolution. // In this case symbols are relocated. Since the change range is `null` all symbols for "test.dfy" are lost. await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "; class Y {}"); - state = await Projects.GetResolvedDocumentAsync(documentItem); + state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem); Assert.NotNull(state); // Relocation happens due to the syntax error; range is null so table is cleared Assert.False(TryFindSymbolDeclarationByName(state, "X", out var _)); @@ -309,19 +309,19 @@ public async Task PassingANullChangeRangePreservesForeignSymbols() { var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Lookup/TestFiles/test.dfy")); await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _)); // Try a change that breaks resolution. Symbols for `foreign.dfy` are kept. await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "; include \"foreign.dfy\"\nclass Y {}"); - document = await Projects.GetResolvedDocumentAsync(documentItem); + document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem); Assert.NotNull(document); Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _)); // Finally we drop the reference to `foreign.dfy` and confirm that `A` is not accessible any more. await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "class Y {}"); - document = await Projects.GetResolvedDocumentAsync(documentItem); + document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem); Assert.NotNull(document); Assert.False(TryFindSymbolDeclarationByName(document, "A", out var _)); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs index 10501a42ea5..33e0f9c22d8 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs @@ -26,7 +26,7 @@ method Test() { }"; var documentItem = CreateTestDocument(source, TestFilePath); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.All(document.GetDiagnostics(), a => Assert.Empty(a.Value)); } @@ -84,6 +84,7 @@ public async Task IndirectlyIncludedFileFailsSyntax() { var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken); Assert.Single(diagnostics); Assert.Contains("the referenced file", diagnostics[0].Message); + Assert.Contains("The first error is:\nrbrace expected", diagnostics[0].Message); Assert.Contains("syntaxError.dfy", diagnostics[0].Message); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs index f6312bf8701..33b2370d428 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs @@ -51,7 +51,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((10, 0), (14, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((7, 10), out var symbol)); Assert.Equal("x", symbol.Name); @@ -90,7 +90,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((12, 0), (14, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((7, 10), out var symbol)); Assert.Equal("x", symbol.Name); @@ -137,7 +137,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((10, 0), (14, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((22, 10), out var symbol)); Assert.Equal("y", symbol.Name); @@ -176,7 +176,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((12, 0), (14, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((16, 10), out var symbol)); Assert.Equal("y", symbol.Name); @@ -203,7 +203,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((6, 10), (6, 10)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((6, 10), out var symbol)); Assert.Equal("x", symbol.Name); @@ -230,7 +230,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((6, 4), (6, 9)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((6, 9), out var symbol)); Assert.Equal("x", symbol.Name); @@ -252,7 +252,7 @@ reads this var change = "y + "; var documentItem = CreateTestDocument(source); await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var originalDocument = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var originalDocument = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(originalDocument); var lookupCountBefore = originalDocument.SignatureAndCompletionTable.LookupTree.Count; @@ -261,7 +261,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((6, 9), (6, 10)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.False(document.SignatureAndCompletionTable.TryGetSymbolAt((6, 9), out var _)); Assert.Equal(lookupCountBefore - 1, document.SignatureAndCompletionTable.LookupTree.Count); @@ -299,7 +299,7 @@ function GetY(): int { " } ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.TryGetSymbolAt((12, 7), out var symbol)); Assert.Equal("x", symbol.Name); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs index 7556a3b10d8..5c211734332 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs @@ -34,7 +34,7 @@ function GetConstant(): int { }".Trim(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.Empty(document.GetDiagnostics()); } @@ -47,7 +47,7 @@ function GetConstant() int { }".Trim(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.Single(document.GetDiagnostics()); var message = document.GetDiagnostics()[documentItem.Uri.ToUri()].ElementAt(0); @@ -62,7 +62,7 @@ function GetConstant(): int { }".Trim(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.Single(document.GetDiagnostics()); var message = document.GetDiagnostics()[documentItem.Uri.ToUri()].ElementAt(0); @@ -103,7 +103,7 @@ method Recurse(x: int) returns (r: int) { await SetUp(options => options.Set(ServerCommand.Verification, VerifyOnMode.Never)); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); } @@ -113,10 +113,11 @@ public async Task EmptyDocumentCanBeOpened() { var source = ""; var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); // Empty files currently yield only a warning. - Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); + var diagnostics = document.GetDiagnostics(); + Assert.True(diagnostics[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); } [Fact] @@ -124,7 +125,7 @@ public async Task DocumentWithNoValidTokensCanBeOpened() { var source = ""; var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); } @@ -134,7 +135,7 @@ public async Task EmptyDocumentCanBeIncluded() { var source = "include \"empty.dfy\""; var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles/test.dfy")); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.False(document.GetDiagnostics().ContainsKey(documentItem.Uri.ToUri())); } diff --git a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs index 008547977d0..3c14701f579 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/SymbolMigrationTest.cs @@ -27,7 +27,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((0, 0), (0, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.Resolved); Assert.Equal(2, document.SignatureAndCompletionTable.Locations.Keys.OfType().Count()); @@ -52,7 +52,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((0, 0), (0, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); } @@ -72,7 +72,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((4, 0), (4, 0)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); } @@ -95,7 +95,7 @@ await ApplyChangeAndWaitCompletionAsync( new Range((1, 0), (1, 11)), change ); - var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri); + var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); Assert.True(document.SignatureAndCompletionTable.Resolved); Assert.Single(document.SignatureAndCompletionTable.Locations.Keys.OfType()); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrder.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs similarity index 91% rename from Source/DafnyLanguageServer.Test/Synchronization/VerificationOrder.cs rename to Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs index b223d846a98..562819ad166 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrder.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; -public class VerificationOrder : ClientBasedLanguageServerTest { +public class VerificationOrderTest : ClientBasedLanguageServerTest { [Fact] public async Task VerificationPriorityBasedOnChangesWorksWithMultipleFiles() { @@ -46,6 +46,6 @@ method Bar() { Assert.Equal(secondFile.Uri.ToUri(), history2[^1].Uri); } - public VerificationOrder(ITestOutputHelper output) : base(output) { + public VerificationOrderTest(ITestOutputHelper output) : base(output) { } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index c5a778774b9..5097bea10ad 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -1,5 +1,6 @@ using System; using System.Collections.Generic; +using System.IO; using System.Linq; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; @@ -14,6 +15,30 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; public class VerificationStatusTest : ClientBasedLanguageServerTest { + [Fact] + public async Task RunWithMultipleSimilarDocuments() { + var source = @" +method Foo() returns (x: int) ensures x / 2 == 1; { + return 2; +}".TrimStart(); + await SetUp(options => { + options.Set(ServerCommand.Verification, VerifyOnMode.Never); + options.Set(ServerCommand.ProjectMode, true); + }); + var directory = Path.GetRandomFileName(); + await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); + var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); + var documentItem2 = await CreateAndOpenTestDocument(source.Replace("Foo", "Bar"), Path.Combine(directory, "RunWithMultipleDocuments2.dfy")); + + var fooRange = new Range(0, 7, 0, 10); + await client.RunSymbolVerification(documentItem1, fooRange.Start, CancellationToken); + + await WaitForStatus(fooRange, PublishedVerificationStatus.Correct, CancellationToken, documentItem1); + + await client.RunSymbolVerification(documentItem2, fooRange.Start, CancellationToken); + await WaitForStatus(fooRange, PublishedVerificationStatus.Correct, CancellationToken, documentItem2); + } + [Fact] public async Task ManuallyRunMethodWithTwoUnderlyingTasks() { var source = @" diff --git a/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs b/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs index baa42523df0..a31ebf40aa1 100644 --- a/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs @@ -1,3 +1,4 @@ +using System; using System.IO; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.Language; @@ -19,7 +20,7 @@ public async Task CancelUnstartedCompilationLeadsToCancelledTasks() { new Mock().Object, new Mock().Object, dafnyOptions, - null, new Compilation(0, new DafnyProject()), null); + null, new Compilation(0, new DafnyProject(), new Uri[] { }), null); compilationManager.CancelPendingUpdates(); await Assert.ThrowsAsync(() => compilationManager.ResolvedCompilation); } diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 948e4b20d54..c39ceac1831 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -66,7 +66,7 @@ private static DocumentTextBuffer CreateTestDocument() { public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { var source = new CancellationTokenSource(); parser.Setup(p => p.Parse( - It.IsAny(), + It.IsAny(), It.IsAny(), It.IsAny())).Callback(() => source.Cancel()) .Throws(); @@ -83,13 +83,13 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { private static Compilation GetCompilation() { var versionedTextDocumentIdentifier = CreateTestDocumentId(); - var compilation = new Compilation(0, ProjectManagerDatabase.ImplicitProject(versionedTextDocumentIdentifier)); + var compilation = new Compilation(0, ProjectManagerDatabase.ImplicitProject(versionedTextDocumentIdentifier.Uri.ToUri()), new[] { versionedTextDocumentIdentifier.Uri.ToUri() }); return compilation; } [Fact] public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() { - parser.Setup(p => p.Parse(It.IsAny(), + parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())) .Throws(); diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 498c272e15b..e58908391fb 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -27,7 +27,7 @@ public class ClientBasedLanguageServerTest : DafnyLanguageServerTestBase, IAsync protected ILanguageClient client; protected TestNotificationReceiver verificationStatusReceiver; - private TestNotificationReceiver compilationStatusReceiver; + protected TestNotificationReceiver compilationStatusReceiver; protected DiagnosticsReceiver diagnosticsReceiver; protected TestNotificationReceiver ghostnessReceiver; @@ -91,12 +91,16 @@ private void AssertMatchRegex(string expected, string value) { } public async Task WaitForStatus(Range nameRange, PublishedVerificationStatus statusToFind, - CancellationToken cancellationToken) { + CancellationToken cancellationToken, [CanBeNull] TextDocumentIdentifier documentIdentifier = null) { while (true) { try { var foundStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(cancellationToken); var namedVerifiableStatus = foundStatus.NamedVerifiables.FirstOrDefault(n => n.NameRange == nameRange); if (namedVerifiableStatus?.Status == statusToFind) { + if (documentIdentifier != null) { + Assert.Equal(documentIdentifier.Uri, foundStatus.Uri); + } + return namedVerifiableStatus; } } catch (OperationCanceledException) { @@ -272,7 +276,7 @@ public async Task AssertNoDiagnosticsAreComing(CancellationToken cancellationTok } protected async Task AssertNoResolutionErrors(TextDocumentItem documentItem) { - var resolutionDiagnostics = (await Projects.GetResolvedDocumentAsync(documentItem))!.GetDiagnostics()[documentItem.Uri.ToUri()].ToList(); + var resolutionDiagnostics = (await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem))!.GetDiagnostics()[documentItem.Uri.ToUri()].ToList(); var resolutionErrors = resolutionDiagnostics.Count(d => d.Severity == DiagnosticSeverity.Error); if (0 != resolutionErrors) { await Console.Out.WriteAsync(string.Join("\n", resolutionDiagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).Select(d => d.ToString()))); diff --git a/Source/DafnyLanguageServer.Test/Util/FileTestExtensions.cs b/Source/DafnyLanguageServer.Test/Util/FileTestExtensions.cs new file mode 100644 index 00000000000..b4772c7d1f1 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Util/FileTestExtensions.cs @@ -0,0 +1,32 @@ +using System.IO; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util; + +public class FileTestExtensions { + + public static async Task WriteWhenUnlocked(string fullPath, string text) { + await using var fs = await WaitForFileToUnlock(fullPath, FileMode.Create, + FileAccess.Write, FileShare.Read); + await using var sw = new StreamWriter(fs); + await sw.WriteAsync(text); + } + + public static async Task WaitForFileToUnlock(string fullPath, FileMode mode, FileAccess access, FileShare share) { + for (int numTries = 0; numTries < 10; numTries++) { + FileStream fs = null; + try { + fs = new FileStream(fullPath, mode, access, share); + return fs; + } catch (IOException) { + if (fs != null) { + await fs.DisposeAsync(); + } + await Task.Delay(50); + } + } + + return null; + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index 08cb95bf214..062b1c77c14 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -1,37 +1,55 @@ using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Microsoft.Dafny.LanguageServer.Workspace; using Microsoft.Dafny.LanguageServer.Workspace.Notifications; -using OmniSharp.Extensions.JsonRpc; -using OmniSharp.Extensions.LanguageServer.Protocol.Client; using System.Threading.Tasks; using JetBrains.Annotations; +using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Xunit; using Xunit.Abstractions; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { [Collection("Sequential Collection")] // Sequential because we saw test failures after switching to parallel execution - public class CompilationStatusNotificationTest : DafnyLanguageServerTestBase, IAsyncLifetime { + public class CompilationStatusNotificationTest : ClientBasedLanguageServerTest { private const int MaxTestExecutionTimeMs = 10000; - private ILanguageClient client; - private TestNotificationReceiver notificationReceiver; - - public Task InitializeAsync() { - return SetUp(null); - } - - public Task DisposeAsync() { - return Task.CompletedTask; - } - - protected async Task SetUp(Action modifyOptions) { - notificationReceiver = new(); - (client, Server) = await Initialize(clientOptions => { - clientOptions.AddHandler(DafnyRequestNames.CompilationStatus, NotificationHandler.For(notificationReceiver.NotificationReceived)); - }, modifyOptions); + [Fact] + public async Task MultipleDocuments() { + var source = @" +method Foo() returns (x: int) ensures x / 2 == 1; { + return 2; +}".TrimStart(); + await SetUp(options => { + options.Set(ServerCommand.ProjectMode, true); + }); + var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); + Directory.CreateDirectory(directory); + await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); + var secondFilePath = Path.Combine(directory, "RunWithMultipleDocuments2.dfy"); + await File.WriteAllTextAsync(secondFilePath, source.Replace("Foo", "Bar")); + var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); + + var expectedStatuses = new[] { + CompilationStatus.Parsing, CompilationStatus.ResolutionStarted, CompilationStatus.CompilationSucceeded, + CompilationStatus.PreparingVerification + }; + var documents = new[] { documentItem1.Uri, DocumentUri.File(secondFilePath) }; + foreach (var expectedStatus in expectedStatuses) { + var statuses = new Dictionary(); + foreach (var _ in documents) { + var statusParams = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); + statuses.Add(statusParams.Uri, statusParams); + } + foreach (var document in documents) { + var status = statuses[document]; + Assert.Equal(expectedStatus, status.Status); + } + } } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -97,7 +115,7 @@ method Abs(x: int) returns (y: int) await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); } private async Task AssertProgress(TextDocumentItem documentItem, CompilationStatus expectedStatus, [CanBeNull] string expectedMessage = null) { - var lastResult = await notificationReceiver.AwaitNextNotificationAsync(CancellationToken); + var lastResult = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.Equal(documentItem.Uri, lastResult.Uri); Assert.Equal(documentItem.Version, lastResult.Version); Assert.Equal(expectedStatus, lastResult.Status); diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index fa13e66a27e..4c6d4bc2d9f 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -111,8 +111,8 @@ public CrashingLoader(ExceptionTests tests, ITextDocumentLoader loader) { this.loader = loader; } - public IdeState CreateUnloaded(DafnyProject project) { - return loader.CreateUnloaded(project); + public IdeState CreateUnloaded(Compilation compilation) { + return loader.CreateUnloaded(compilation); } public Task LoadAsync(DafnyOptions options, Compilation compilation, diff --git a/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs b/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs index dd937d46254..1f8f28c0412 100644 --- a/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/StabilityTest.cs @@ -36,14 +36,14 @@ public Task DisposeAsync() { public async Task GhcMergeSort() { var documentItem = await CreateTextDocumentFromFileAsync("GHC-MergeSort.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - Assert.NotNull(await Projects.GetResolvedDocumentAsync(documentItem.Uri)); + Assert.NotNull(await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri)); } [Fact(Timeout = MaxTestExecutionTimeMs)] public async Task GenericSort() { var documentItem = await CreateTextDocumentFromFileAsync("GenericSort.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - Assert.NotNull(await Projects.GetResolvedDocumentAsync(documentItem.Uri)); + Assert.NotNull(await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri)); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -56,7 +56,7 @@ method NestedExpression() { }"; var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - Assert.NotNull(await Projects.GetResolvedDocumentAsync(documentItem.Uri)); + Assert.NotNull(await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri)); } public StabilityTest(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer/Handlers/Custom/VerificationHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/VerificationHandler.cs index 54671c9d106..8d94e56f463 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/VerificationHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/VerificationHandler.cs @@ -36,19 +36,22 @@ public async Task Handle(VerificationParams request, CancellationToken can } var translatedCompilation = await projectManager.CompilationManager.TranslatedCompilation; - var requestPosition = request.Position; var someTasksAreRunning = false; - var tasksAtPosition = GetTasksAtPosition(translatedCompilation, requestPosition); + var tasksAtPosition = GetTasksAtPosition(translatedCompilation, request); foreach (var taskToRun in tasksAtPosition) { someTasksAreRunning |= projectManager.CompilationManager.VerifyTask(translatedCompilation, taskToRun); } return someTasksAreRunning; } - private static IEnumerable GetTasksAtPosition(CompilationAfterTranslation compilation, Position requestPosition) { + private static IEnumerable GetTasksAtPosition(CompilationAfterTranslation compilation, TextDocumentPositionParams request) { + var uri = request.TextDocument.Uri.ToUri(); return compilation.VerificationTasks.Where(t => { + if (((IToken)t.Implementation.tok).Uri != uri) { + return false; + } var lspPosition = t.Implementation.tok.GetLspPosition(); - return lspPosition.Equals(requestPosition); + return lspPosition.Equals(request.Position); }); } @@ -59,8 +62,7 @@ public async Task Handle(CancelVerificationParams request, CancellationTok } var translatedDocument = await projectManager.CompilationManager.TranslatedCompilation; - var requestPosition = request.Position; - foreach (var taskToRun in GetTasksAtPosition(translatedDocument, requestPosition)) { + foreach (var taskToRun in GetTasksAtPosition(translatedDocument, request)) { taskToRun.Cancel(); } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index b77206b1ea8..666be22f9e9 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -43,7 +43,7 @@ public override Task Handle(CompletionItem request, Cancellation public override async Task Handle(CompletionParams request, CancellationToken cancellationToken) { logger.LogDebug("Completion params received"); - var document = await projects.GetResolvedDocumentAsync(request.TextDocument); + var document = await projects.GetResolvedDocumentAsyncNormalizeUri(request.TextDocument); if (document == null) { logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return new CompletionList(); diff --git a/Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs index 4188b58780a..dbb3683275e 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyDefinitionHandler.cs @@ -27,7 +27,7 @@ protected override DefinitionRegistrationOptions CreateRegistrationOptions(Defin } public override async Task Handle(DefinitionParams request, CancellationToken cancellationToken) { - var state = await projects.GetResolvedDocumentAsync(request.TextDocument); + var state = await projects.GetResolvedDocumentAsyncNormalizeUri(request.TextDocument); if (state == null) { logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return new LocationOrLocationLinks(); diff --git a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs index 06c76330df8..ca21b76f5e5 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs @@ -31,7 +31,7 @@ protected override DocumentSymbolRegistrationOptions CreateRegistrationOptions(D } public override async Task Handle(DocumentSymbolParams request, CancellationToken cancellationToken) { - var document = await projects.GetResolvedDocumentAsync(request.TextDocument); + var document = await projects.GetResolvedDocumentAsyncNormalizeUri(request.TextDocument); if (document == null) { logger.LogWarning("symbols requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return EmptySymbols; diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index 656578eba55..84b18f19cc8 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -41,7 +41,7 @@ protected override HoverRegistrationOptions CreateRegistrationOptions(HoverCapab public override async Task Handle(HoverParams request, CancellationToken cancellationToken) { logger.LogDebug("received hover request for {Document}", request.TextDocument); - var document = await projects.GetResolvedDocumentAsync(request.TextDocument); + var document = await projects.GetResolvedDocumentAsyncInternal(request.TextDocument); if (document == null) { logger.LogWarning("the document {Document} is not loaded", request.TextDocument); return null; diff --git a/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs index 0acd26c6214..d5b46676b6d 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs @@ -33,7 +33,7 @@ protected override SignatureHelpRegistrationOptions CreateRegistrationOptions(Si public override async Task Handle(SignatureHelpParams request, CancellationToken cancellationToken) { logger.LogDebug("received signature request for document {DocumentUri}", request.TextDocument.Uri); - var document = await projects.GetResolvedDocumentAsync(request.TextDocument); + var document = await projects.GetResolvedDocumentAsyncNormalizeUri(request.TextDocument); if (document == null) { logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return null; diff --git a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs index 095825b9f1f..d94e0235b7b 100644 --- a/Source/DafnyLanguageServer/Language/DafnyLangParser.cs +++ b/Source/DafnyLanguageServer/Language/DafnyLangParser.cs @@ -32,12 +32,12 @@ public DafnyLangParser(DafnyOptions options, IFileSystem fileSystem, ITelemetryP cachingParser = new CachingParser(innerParserLogger, fileSystem); } - public Program Parse(DafnyProject project, ErrorReporter reporter, CancellationToken cancellationToken) { + public Program Parse(Compilation compilation, ErrorReporter reporter, CancellationToken cancellationToken) { mutex.Wait(cancellationToken); var beforeParsing = DateTime.Now; try { - var rootSourceUris = project.GetRootSourceUris(fileSystem, options).Concat(options.CliRootSourceUris).ToList(); + var rootSourceUris = compilation.RootUris; List dafnyFiles = new(); foreach (var rootSourceUri in rootSourceUris) { try { @@ -46,12 +46,12 @@ public Program Parse(DafnyProject project, ErrorReporter reporter, CancellationT logger.LogError($"Tried to parse file {rootSourceUri} that could not be found"); } } - var result = cachingParser.ParseFiles(project.ProjectName, dafnyFiles, reporter, cancellationToken); + var result = cachingParser.ParseFiles(compilation.Project.ProjectName, dafnyFiles, reporter, cancellationToken); cachingParser.Prune(); return result; } finally { - telemetryPublisher.PublishTime("Parse", project.Uri.ToString(), DateTime.Now - beforeParsing); + telemetryPublisher.PublishTime("Parse", compilation.Project.Uri.ToString(), DateTime.Now - beforeParsing); mutex.Release(); } } diff --git a/Source/DafnyLanguageServer/Language/IDafnyParser.cs b/Source/DafnyLanguageServer/Language/IDafnyParser.cs index c8483445ed6..3f4ed95439a 100644 --- a/Source/DafnyLanguageServer/Language/IDafnyParser.cs +++ b/Source/DafnyLanguageServer/Language/IDafnyParser.cs @@ -11,7 +11,7 @@ namespace Microsoft.Dafny.LanguageServer.Language { /// Any implementation has to guarantee thread-safety of its public members. /// public interface IDafnyParser { - Program Parse(DafnyProject project, ErrorReporter reporter, + Program Parse(Compilation compilation, ErrorReporter reporter, CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs index ff54c3cf400..b89b44a3c77 100644 --- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs @@ -33,12 +33,12 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv serviceProvider.GetRequiredService>(), serviceProvider.GetRequiredService>())) .AddSingleton() - .AddSingleton(serviceProvider => documentIdentifier => + .AddSingleton(serviceProvider => compilation => new IdeStateObserver(serviceProvider.GetRequiredService>(), serviceProvider.GetRequiredService(), serviceProvider.GetRequiredService(), serviceProvider.GetRequiredService(), - documentIdentifier)) + compilation)) .AddSingleton() .AddSingleton(CreateVerifier) .AddSingleton(serviceProvider => (options, engine, compilation, migratedVerificationTree) => new CompilationManager( diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs index 1f45f7f07ec..3ae02aaced6 100644 --- a/Source/DafnyLanguageServer/ServerCommand.cs +++ b/Source/DafnyLanguageServer/ServerCommand.cs @@ -19,6 +19,7 @@ static ServerCommand() { DafnyOptions.RegisterLegacyBinding(VerifySnapshots, (options, u) => options.VerifySnapshots = (int)u); DooFile.RegisterNoChecksNeeded( + ProjectMode, Verification, GhostIndicators, LineVerificationStatus, @@ -42,7 +43,7 @@ static ServerCommand() { Send notifications about the verification status of each line in the program. ".TrimStart()); - public static readonly Option ProjectMode = new("--project-mode", + public static readonly Option ProjectMode = new("--project-mode", () => false, "New mode with working with project files. Will become the default") { IsHidden = true }; @@ -60,6 +61,7 @@ related locations }; public IEnumerable