From fb8b5f26d875bc86d4cca4e1a335ea513a1b7af3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 17:17:41 +0200 Subject: [PATCH] Move compilation status updates to notification publisher (#4454) Fixes #4451 ### Changes - symbolStatus notifications are resent after any document change is made. - "Parsing" is no longer sent when opening a file because it's the default state for a file. This requires an update on the client to return to the old behavior, but in the meantime it's OK for the client to have this tiny regression. - "Preparing Verification" no longer exists as a notification. Because one verifiable can be preparing verification while another is verifying, there is no longer a global "Preparing verification" state so this notification lost its meaning. We can bring something like this back but on a more granular level. - "Resolution Succeeded (not verified)" (UI name) / CompilationSucceeded (server name) no longer exists as a notification. This sat between ResolutionStarted and symbolStatus notifications that indicated which symbols could be verified, but in practice was never shown because immediately after it symbolStatus notifications would be sent that trigger a status like "Verified X declarations, skipped Y" - `CompilationManager` no longer sends any status updates to the IDE client, bringing it closer to being able to be moved to `DafnyCore` and used by the CLI. ### Testing - Updated automating tests 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). --- .../DeclarationLocationMigrationTest.cs | 2 +- .../Synchronization/IncludeFileTest.cs | 2 +- .../Synchronization/LookupMigrationTest.cs | 2 +- .../Synchronization/OpenDocumentTest.cs | 25 +++--- .../Synchronization/VerificationStatusTest.cs | 2 + .../Unit/CompilationManagerTest.cs | 2 - .../Unit/TextDocumentLoaderTest.cs | 5 -- .../Util/ClientBasedLanguageServerTest.cs | 7 +- .../CompilationStatusNotificationTest.cs | 37 +++----- .../Various/ExceptionTests.cs | 7 +- .../Handlers/DafnyHoverHandler.cs | 2 +- .../Language/LanguageServerExtensions.cs | 2 - .../Workspace/CompilationManager.cs | 8 -- .../CompilationStatusNotificationPublisher.cs | 31 ------- .../Workspace/Documents/Compilation.cs | 3 + .../Documents/CompilationAfterResolution.cs | 11 ++- .../Workspace/FileVerificationStatus.cs | 16 ++++ ...ICompilationStatusNotificationPublisher.cs | 14 --- .../DafnyLanguageServer/Workspace/IdeState.cs | 26 ++++-- .../Workspace/IdeStateObserver.cs | 45 +++++----- .../Workspace/LanguageServerExtensions.cs | 14 +-- .../Workspace/NotificationPublisher.cs | 85 ++++++++++++++----- .../Notifications/CompilationStatus.cs | 4 +- .../Workspace/TextDocumentLoader.cs | 23 +---- 24 files changed, 175 insertions(+), 200 deletions(-) delete mode 100644 Source/DafnyLanguageServer/Workspace/CompilationStatusNotificationPublisher.cs delete mode 100644 Source/DafnyLanguageServer/Workspace/ICompilationStatusNotificationPublisher.cs diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs index aff89f19f3d..5f81dfaeff5 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs @@ -126,7 +126,7 @@ await ApplyChangeAndWaitCompletionAsync( Assert.Equal(new Range((10, 6), (10, 7)), location.Name); Assert.Equal(new Range((10, 0), (11, 0)), location.Declaration); } catch (AssertActualExpectedException) { - await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetDiagnostics().Values.Stringify()}"); + await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetAllDiagnostics().Stringify()}"); var programString = new StringWriter(); var printer = new Printer(programString, DafnyOptions.Default); printer.PrintProgram((Program)state.Program, true); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs index a6e74d146ec..0141d65ab1f 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs @@ -28,7 +28,7 @@ method Test() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.All(document.GetDiagnostics(), a => Assert.Empty(a.Value)); + Assert.Empty(document.GetAllDiagnostics()); } // https://github.com/dafny-lang/language-server-csharp/issues/40 diff --git a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs index 594630e8b40..3c5996bf6bf 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs @@ -148,7 +148,7 @@ await ApplyChangeAndWaitCompletionAsync( Assert.True(state.SignatureAndCompletionTable.TryGetSymbolAt((22, 10), out var symbol)); Assert.Equal("y", symbol.Name); } catch (AssertActualExpectedException) { - await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetDiagnostics().Values.Stringify()}"); + await output.WriteLineAsync($"state version is {state.Version}, diagnostics: {state.GetAllDiagnostics().Stringify()}"); var programString = new StringWriter(); var printer = new Printer(programString, DafnyOptions.Default); printer.PrintProgram((Program)state.Program, true); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs index d4d66ef9c1d..db41bc9a9e7 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs @@ -23,7 +23,7 @@ public Task DisposeAsync() { } private async Task SetUp(Action modifyOptions) { - (client, Server) = await Initialize(options => { }, modifyOptions); + (client, Server) = await Initialize(_ => { }, modifyOptions); } [Fact] @@ -34,9 +34,9 @@ function GetConstant(): int { }".Trim(); var documentItem = CreateTestDocument(source, "CorrectDocumentCanBeParsedResolvedAndVerifiedWithoutErrors.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); - Assert.NotNull(document); - Assert.True(document.GetDiagnostics().Values.All(x => !x.Any())); + var state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); + Assert.NotNull(state); + Assert.Empty(state.GetAllDiagnostics()); } [Fact] @@ -49,8 +49,8 @@ function GetConstant() int { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.Single(document.GetDiagnostics()); - var message = document.GetDiagnostics()[documentItem.Uri.ToUri()].ElementAt(0); + Assert.Single(document.GetDiagnosticUris()); + var message = document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).ElementAt(0); Assert.Equal(MessageSource.Parser.ToString(), message.Source); } @@ -64,8 +64,8 @@ function GetConstant(): int { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.Single(document.GetDiagnostics()); - var message = document.GetDiagnostics()[documentItem.Uri.ToUri()].ElementAt(0); + Assert.Single(document.GetDiagnosticUris()); + var message = document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).ElementAt(0); Assert.Equal(MessageSource.Resolver.ToString(), message.Source); } @@ -105,7 +105,7 @@ method Recurse(x: int) returns (r: int) { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); + Assert.True(document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).All(d => d.Severity != DiagnosticSeverity.Error)); } [Fact] @@ -116,8 +116,7 @@ public async Task EmptyDocumentCanBeOpened() { var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); // Empty files currently yield only a warning. - var diagnostics = document.GetDiagnostics(); - Assert.True(diagnostics[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); + Assert.True(document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).All(d => d.Severity != DiagnosticSeverity.Error)); } [Fact] @@ -127,7 +126,7 @@ public async Task DocumentWithNoValidTokensCanBeOpened() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.True(document.GetDiagnostics()[documentItem.Uri.ToUri()].All(d => d.Severity != DiagnosticSeverity.Error)); + Assert.True(document.GetDiagnosticsForUri(documentItem.Uri.ToUri()).All(d => d.Severity != DiagnosticSeverity.Error)); } [Fact] @@ -137,7 +136,7 @@ public async Task EmptyDocumentCanBeIncluded() { await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri); Assert.NotNull(document); - Assert.False(document.GetDiagnostics().ContainsKey(documentItem.Uri.ToUri())); + Assert.DoesNotContain(documentItem.Uri.ToUri(), document.GetDiagnosticUris()); } public OpenDocumentTest(ITestOutputHelper output) : base(output) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index ef970cf0722..55ac3ce9137 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -343,6 +343,8 @@ await SetUp(options => { }); var documentItem = CreateTestDocument(source, "WhenUsingOnSaveMethodStaysStaleUntilSave.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var stale1 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); + Assert.Equal(PublishedVerificationStatus.Stale, stale1.NamedVerifiables[0].Status); // Send a change to enable getting a new status notification. ApplyChange(ref documentItem, new Range(new Position(1, 0), new Position(1, 0)), "\n"); diff --git a/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs b/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs index c00660fd0a9..951bc8bfd0e 100644 --- a/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs @@ -15,9 +15,7 @@ public async Task CancelUnstartedCompilationLeadsToCancelledTasks() { var dafnyOptions = DafnyOptions.Create(TextWriter.Null, TextReader.Null); var compilationManager = new CompilationManager(new Mock>().Object, new Mock().Object, - new Mock().Object, new Mock().Object, - new Mock().Object, new Mock().Object, dafnyOptions, null, new Compilation(0, new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }, new Uri[] { }), null); diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 0a2c5d48de1..c18ccd95afa 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -23,10 +23,8 @@ public class TextDocumentLoaderTest { private Mock symbolResolver; private Mock symbolTableFactory; private Mock ghostStateDiagnosticCollector; - private Mock notificationPublisher; private TextDocumentLoader textDocumentLoader; private Mock> logger; - private Mock diagnosticPublisher; public TextDocumentLoaderTest(ITestOutputHelper output) { this.output = new WriterFromOutputHelper(output); @@ -34,16 +32,13 @@ public TextDocumentLoaderTest(ITestOutputHelper output) { symbolResolver = new(); symbolTableFactory = new(); ghostStateDiagnosticCollector = new(); - notificationPublisher = new(); fileSystem = new(); logger = new Mock>(); - diagnosticPublisher = new Mock(); textDocumentLoader = TextDocumentLoader.Create( parser.Object, symbolResolver.Object, symbolTableFactory.Object, ghostStateDiagnosticCollector.Object, - notificationPublisher.Object, logger.Object ); } diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index c1895ad4797..13c7c976aa9 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -94,12 +94,12 @@ private void AssertMatchRegex(string expected, string value) { } } - public async Task WaitForStatus(Range nameRange, PublishedVerificationStatus statusToFind, + public async Task WaitForStatus([CanBeNull] Range nameRange, PublishedVerificationStatus statusToFind, CancellationToken cancellationToken, [CanBeNull] TextDocumentIdentifier documentIdentifier = null) { while (true) { try { var foundStatus = await verificationStatusReceiver.AwaitNextNotificationAsync(cancellationToken); - var namedVerifiableStatus = foundStatus.NamedVerifiables.FirstOrDefault(n => n.NameRange == nameRange); + var namedVerifiableStatus = foundStatus.NamedVerifiables.FirstOrDefault(n => nameRange == null || n.NameRange == nameRange); if (namedVerifiableStatus?.Status == statusToFind) { if (documentIdentifier != null) { Assert.Equal(documentIdentifier.Uri, foundStatus.Uri); @@ -313,9 +313,8 @@ public async Task AssertNoDiagnosticsAreComing(CancellationToken cancellationTok } protected async Task AssertNoResolutionErrors(TextDocumentItem documentItem) { - var fullDiagnostics = (await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem))!.GetDiagnostics(); + var resolutionDiagnostics = (await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem))!.GetDiagnosticsForUri(documentItem.Uri.ToUri()).ToList(); // A document without diagnostics may be absent, even if resolved successfully - var resolutionDiagnostics = fullDiagnostics.GetValueOrDefault(documentItem.Uri.ToUri(), ImmutableList.Empty); 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/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index c5335c4eb9e..c8149e35b49 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -21,7 +21,7 @@ public class CompilationStatusNotificationTest : ClientBasedLanguageServerTest { [Fact] public async Task MultipleDocuments() { var source = @" -method Foo() returns (x: int) ensures x / 2 == 1; { +method Foo() returns (x: int) { return 2; }".TrimStart(); var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); @@ -32,8 +32,7 @@ public async Task MultipleDocuments() { var documentItem1 = await CreateAndOpenTestDocument(source, Path.Combine(directory, "RunWithMultipleDocuments1.dfy")); var expectedStatuses = new[] { - CompilationStatus.Parsing, CompilationStatus.ResolutionStarted, CompilationStatus.CompilationSucceeded, - CompilationStatus.PreparingVerification + CompilationStatus.ResolutionStarted }; var documents = new[] { documentItem1.Uri, DocumentUri.File(secondFilePath) }; foreach (var expectedStatus in expectedStatuses) { @@ -47,6 +46,9 @@ public async Task MultipleDocuments() { Assert.Equal(expectedStatus, status.Status); } } + foreach (var _ in documents) { + await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken); + } } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -60,13 +62,11 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source, "DocumentWithParserErrorsSendsParsingFailedStatus.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ParsingFailed); // We re-send the same erroneous document again to check that we don't have a CompilationSucceeded event queued. var otherDoc = CreateTestDocument(source, "Test2.dfy"); client.OpenDocument(otherDoc); - await AssertProgress(otherDoc, CompilationStatus.Parsing); await AssertProgress(otherDoc, CompilationStatus.ParsingFailed); } @@ -81,14 +81,12 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source, "DocumentWithResolverErrorsSendsResolutionFailedStatus.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.ResolutionFailed); // We re-send the same erroneous document again to check that we don't have a CompilationSucceeded event queued. var otherDoc = CreateTestDocument(source, "Test2.dfy"); client.OpenDocument(otherDoc); - await AssertProgress(otherDoc, CompilationStatus.Parsing); await AssertProgress(otherDoc, CompilationStatus.ResolutionStarted); await AssertProgress(otherDoc, CompilationStatus.ResolutionFailed); } @@ -107,9 +105,8 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source, "DocumentWithoutErrorsSendsCompilationSucceededVerificationStartedAndVerificationSucceededStatuses.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Correct, CancellationToken, documentItem); } private async Task AssertProgress(TextDocumentItem documentItem, CompilationStatus expectedStatus, [CanBeNull] string expectedMessage = null) { var lastResult = await compilationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); @@ -132,18 +129,16 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source, "DocumentWithOnlyVerifierErrorsSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem); } [Fact(Timeout = MaxTestExecutionTimeMs)] public async Task DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() { var documentItem = CreateTestDocument(SlowToVerify, "DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -151,9 +146,8 @@ public async Task DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucce await SetUp(options => options.Set(BoogieOptionBag.VerificationTimeLimit, 3U)); var documentItem = CreateTestDocument(SlowToVerify, "DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -171,14 +165,12 @@ method Abs(x: int) returns (y: int) // compilation status twice without any verification status inbetween. var documentItem1 = CreateTestDocument(source, "test_1.dfy"); await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken); - await AssertProgress(documentItem1, CompilationStatus.Parsing); await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1); var documentItem2 = CreateTestDocument(source, "test_2dfy"); await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken); - await AssertProgress(documentItem2, CompilationStatus.Parsing); await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -197,15 +189,13 @@ method Abs(x: int) returns (y: int) var documentItem1 = CreateTestDocument(source, "test_1.dfy"); await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken); await client.SaveDocumentAndWaitAsync(documentItem1, CancellationToken); - await AssertProgress(documentItem1, CompilationStatus.Parsing); await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem1); var documentItem2 = CreateTestDocument(source, "test_2dfy"); await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken); await client.SaveDocumentAndWaitAsync(documentItem2, CancellationToken); - await AssertProgress(documentItem2, CompilationStatus.Parsing); await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded); + await WaitForStatus(null, PublishedVerificationStatus.Stale, CancellationToken, documentItem2); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -219,7 +209,6 @@ lemma Something(i: int) }"; var documentItem = CreateTestDocument(source, "MultisetShouldNotCrashParser.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ParsingFailed); } diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index 45af2653147..0bd90df8ebb 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -27,8 +27,9 @@ public class ExceptionTests : ClientBasedLanguageServerTest { protected override void ServerOptionsAction(LanguageServerOptions serverOptions) { serverOptions.Services + .AddSingleton() .AddSingleton(serviceProvider => new CrashingLoader(this, - LanguageServerExtensions.CreateTextDocumentLoader(serviceProvider))) + serviceProvider.GetRequiredService())) .AddSingleton(serviceProvider => new CrashingVerifier(this, new DafnyProgramVerifier(serviceProvider.GetRequiredService>()) )); @@ -106,9 +107,9 @@ public Task> GetVerificationTasksAsync(Execut class CrashingLoader : ITextDocumentLoader { private readonly ExceptionTests tests; - private readonly ITextDocumentLoader loader; + private readonly TextDocumentLoader loader; - public CrashingLoader(ExceptionTests tests, ITextDocumentLoader loader) { + public CrashingLoader(ExceptionTests tests, TextDocumentLoader loader) { this.tests = tests; this.loader = loader; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index ce1cdf482cb..4586fcb1b42 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -93,7 +93,7 @@ public int Compare(AssertionBatchIndex? key1, AssertionBatchIndex? key2) { private string? GetDiagnosticsHover(IdeState state, Uri uri, Position position, out bool areMethodStatistics) { areMethodStatistics = false; - var uriDiagnostics = state.GetDiagnostics().GetOrDefault(uri, Enumerable.Empty).ToList(); + var uriDiagnostics = state.GetDiagnosticsForUri(uri).ToList(); foreach (var diagnostic in uriDiagnostics) { if (diagnostic.Range.Contains(position)) { string? detail = ErrorRegistry.GetDetail(diagnostic.Code); diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs index 0be23876b54..007daa89941 100644 --- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs @@ -45,9 +45,7 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv .AddSingleton(serviceProvider => (options, engine, compilation, migratedVerificationTree) => new CompilationManager( serviceProvider.GetRequiredService>(), serviceProvider.GetRequiredService(), - serviceProvider.GetRequiredService(), serviceProvider.GetRequiredService(), - serviceProvider.GetRequiredService(), serviceProvider.GetRequiredService(), options, engine, compilation, migratedVerificationTree )) diff --git a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs index 38c08591dd6..68fe980d4c0 100644 --- a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs +++ b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs @@ -37,8 +37,6 @@ public class CompilationManager { private readonly ILogger logger; private readonly ITextDocumentLoader documentLoader; - private readonly ICompilationStatusNotificationPublisher statusPublisher; - private readonly INotificationPublisher notificationPublisher; private readonly IProgramVerifier verifier; private readonly IVerificationProgressReporter verificationProgressReporter; @@ -63,9 +61,7 @@ public class CompilationManager { public CompilationManager( ILogger logger, ITextDocumentLoader documentLoader, - INotificationPublisher notificationPublisher, IProgramVerifier verifier, - ICompilationStatusNotificationPublisher statusPublisher, IVerificationProgressReporter verificationProgressReporter, DafnyOptions options, ExecutionEngine boogieEngine, @@ -79,9 +75,7 @@ IReadOnlyDictionary migratedVerificationTrees this.documentLoader = documentLoader; this.logger = logger; - this.notificationPublisher = notificationPublisher; this.verifier = verifier; - this.statusPublisher = statusPublisher; this.verificationProgressReporter = verificationProgressReporter; cancellationSource = new(); cancellationSource.Token.Register(() => started.TrySetCanceled(cancellationSource.Token)); @@ -172,7 +166,6 @@ public async Task VerifySymbol(FilePosition verifiableLocation, bool actua IReadOnlyDictionary> tasksForModule; try { tasksForModule = await compilation.TranslatedModules.GetOrAdd(containingModule, async m => { - _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.PreparingVerification); var result = await verifier.GetVerificationTasksAsync(boogieEngine, compilation, containingModule, cancellationSource.Token); compilation.ResolutionDiagnostics = ((DiagnosticErrorReporter)compilation.Program.Reporter).AllDiagnosticsCopy; @@ -211,7 +204,6 @@ public async Task VerifySymbol(FilePosition verifiableLocation, bool actua } if (actuallyVerifyTasks) { - var tasks = implementations.Values.Select(t => t.Task).ToList(); foreach (var task in tasks) { diff --git a/Source/DafnyLanguageServer/Workspace/CompilationStatusNotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/CompilationStatusNotificationPublisher.cs deleted file mode 100644 index aa04ac65a8f..00000000000 --- a/Source/DafnyLanguageServer/Workspace/CompilationStatusNotificationPublisher.cs +++ /dev/null @@ -1,31 +0,0 @@ -using System.Threading.Tasks; -using Microsoft.Dafny.LanguageServer.Workspace.Notifications; -using OmniSharp.Extensions.LanguageServer.Protocol.Server; - -namespace Microsoft.Dafny.LanguageServer.Workspace { - public class CompilationStatusNotificationPublisher : ICompilationStatusNotificationPublisher { - private readonly ITextDocumentLanguageServer languageServer; - private readonly IProjectDatabase projectDatabase; - - public CompilationStatusNotificationPublisher(ITextDocumentLanguageServer languageServer, IProjectDatabase projectDatabase) { - this.languageServer = languageServer; - this.projectDatabase = projectDatabase; - } - - public async Task SendStatusNotification(Compilation compilation, CompilationStatus status, - string? message = null) { - foreach (var uri in compilation.RootUris) { - var uriProject = await projectDatabase.GetProject(uri); - var ownedUri = uriProject.Equals(compilation.Project); - if (ownedUri) { - languageServer.SendNotification(new CompilationStatusParams { - Uri = uri, - Version = compilation.Version, - Status = status, - Message = message - }); - } - } - } - } -} diff --git a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs index 97ecc0eb365..8ad86d8a4b4 100644 --- a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs @@ -23,6 +23,9 @@ namespace Microsoft.Dafny.LanguageServer.Workspace { /// There can be different verification threads that update the state of this object. /// public class Compilation { + /// + /// These do not have to be owned + /// public IReadOnlyList RootUris { get; } public int Version { get; } public DafnyProject Project { get; } diff --git a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs index e9a09946593..34f6b3fec61 100644 --- a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs +++ b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs @@ -74,8 +74,9 @@ IdeVerificationResult MergeResults(IEnumerable results) { public override IdeState ToIdeState(IdeState previousState) { IdeVerificationResult MergeVerifiable(ICanVerify canVerify) { - var location = canVerify.NameToken.GetLocation(); - var previousForCanVerify = previousState.VerificationResults.GetValueOrDefault(location) ?? new(false, ImmutableDictionary.Empty); + var range = canVerify.NameToken.GetLspRange(); + var previousForCanVerify = previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range) ?? + new(false, ImmutableDictionary.Empty); if (!ImplementationsPerVerifiable.TryGetValue(canVerify, out var implementationsPerName)) { return previousForCanVerify with { Implementations = previousForCanVerify.Implementations.ToDictionary(kv => kv.Key, kv => kv.Value with { @@ -108,8 +109,10 @@ IdeVerificationResult MergeVerifiable(ICanVerify canVerify) { GhostRanges = GhostDiagnostics, Counterexamples = new List(Counterexamples), VerificationTrees = VerificationTrees.ToDictionary(kv => kv.Key, kv => kv.Value.GetCopyForNotification()), - VerificationResults = Verifiables.GroupBy(l => l.NameToken.GetLocation()).ToDictionary(k => k.Key, - k => MergeResults(k.Select(MergeVerifiable))) + VerificationResults = Verifiables.GroupBy(l => l.NameToken.Uri).ToDictionary(k => k.Key, + k => k.GroupBy(l => l.NameToken.GetLspRange()).ToDictionary( + l => l.Key, + l => MergeResults(l.Select(MergeVerifiable)))) }; return result; } diff --git a/Source/DafnyLanguageServer/Workspace/FileVerificationStatus.cs b/Source/DafnyLanguageServer/Workspace/FileVerificationStatus.cs index cf0b07e0779..c8ef9321223 100644 --- a/Source/DafnyLanguageServer/Workspace/FileVerificationStatus.cs +++ b/Source/DafnyLanguageServer/Workspace/FileVerificationStatus.cs @@ -14,6 +14,22 @@ public record FileVerificationStatus( public override string ToString() { return $"{nameof(NamedVerifiables)}: {string.Join(", ", NamedVerifiables)}"; } + + public virtual bool Equals(FileVerificationStatus? other) { + if (ReferenceEquals(null, other)) { + return false; + } + + if (ReferenceEquals(this, other)) { + return true; + } + + return NamedVerifiables.SequenceEqual(other.NamedVerifiables); + } + + public override int GetHashCode() { + return 0; + } } /** diff --git a/Source/DafnyLanguageServer/Workspace/ICompilationStatusNotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/ICompilationStatusNotificationPublisher.cs deleted file mode 100644 index 817cc3a192b..00000000000 --- a/Source/DafnyLanguageServer/Workspace/ICompilationStatusNotificationPublisher.cs +++ /dev/null @@ -1,14 +0,0 @@ -using System.Threading.Tasks; -using Microsoft.Dafny.LanguageServer.Workspace.Notifications; -using OmniSharp.Extensions.LanguageServer.Protocol.Document; -using OmniSharp.Extensions.LanguageServer.Protocol.Models; - -namespace Microsoft.Dafny.LanguageServer.Workspace { - /// - /// Implementations of this interface are responsible to publish the compilation - /// status of a to the LSP client. - /// - public interface ICompilationStatusNotificationPublisher { - Task SendStatusNotification(Compilation compilation, CompilationStatus status, string? message = null); - } -} diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 16f044d03a6..7b6bfffe19d 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -29,17 +29,31 @@ public record IdeState( IReadOnlyDictionary> ResolutionDiagnostics, SymbolTable SymbolTable, LegacySignatureAndCompletionTable SignatureAndCompletionTable, - Dictionary VerificationResults, + Dictionary> VerificationResults, IReadOnlyList Counterexamples, IReadOnlyDictionary> GhostRanges, IReadOnlyDictionary VerificationTrees ) { - public ImmutableDictionary> GetDiagnostics() { - var resolutionDiagnostics = ResolutionDiagnostics.ToImmutableDictionary(); - var verificationDiagnostics = VerificationResults.GroupBy(kv => kv.Key.Uri).Select(kv => - new KeyValuePair>(kv.Key.ToUri(), kv.SelectMany(x => x.Value.Implementations.Values.SelectMany(v => v.Diagnostics)).ToList())); - return resolutionDiagnostics.Merge(verificationDiagnostics, Lists.Concat); + + public IReadOnlyDictionary GetVerificationResults(Uri uri) { + return VerificationResults.GetValueOrDefault(uri) ?? + ((IReadOnlyDictionary)ImmutableDictionary.Empty); + } + + public IEnumerable GetAllDiagnostics() { + return GetDiagnosticUris().SelectMany(GetDiagnosticsForUri); + } + + public IEnumerable GetDiagnosticsForUri(Uri uri) { + var resolutionDiagnostics = ResolutionDiagnostics.GetValueOrDefault(uri) ?? Enumerable.Empty(); + var verificationDiagnostics = GetVerificationResults(uri).SelectMany(x => + x.Value.Implementations.Values.SelectMany(v => v.Diagnostics)); + return resolutionDiagnostics.Concat(verificationDiagnostics); + } + + public IEnumerable GetDiagnosticUris() { + return ResolutionDiagnostics.Keys.Concat(VerificationResults.Keys); } } diff --git a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs index cca01c24f37..2fd77fb5817 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs @@ -101,30 +101,31 @@ public void Migrate(Migrator migrator, int version) { } } - private Dictionary MigrateImplementationViews(Migrator migrator, - Dictionary oldVerificationDiagnostics) { - var result = new Dictionary(); - foreach (var entry in oldVerificationDiagnostics) { - var newOuterRange = migrator.MigrateRange(entry.Key.Range); - if (newOuterRange == null) { - continue; - } + private Dictionary> MigrateImplementationViews(Migrator migrator, + Dictionary> oldVerificationDiagnostics) { + return oldVerificationDiagnostics.ToDictionary(kv => kv.Key, kv => { + var result = new Dictionary(); + foreach (var entry in kv.Value) { + var newOuterRange = migrator.MigrateRange(entry.Key); + if (newOuterRange == null) { + continue; + } - var newValue = new Dictionary(); - foreach (var innerEntry in entry.Value.Implementations) { - var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range); - if (newInnerRange != null) { - newValue.Add(innerEntry.Key, innerEntry.Value with { - Range = newInnerRange, - Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics) - }); + var newValue = new Dictionary(); + foreach (var innerEntry in entry.Value.Implementations) { + var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range); + if (newInnerRange != null) { + newValue.Add(innerEntry.Key, innerEntry.Value with { + Range = newInnerRange, + Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics) + }); + } } + + result.Add(newOuterRange, entry.Value with { Implementations = newValue }); } - result.Add(new Location() { - Uri = entry.Key.Uri, - Range = newOuterRange - }, entry.Value with { Implementations = newValue }); - } - return result; + + return result; + }); } } diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs index a3d054c5681..98aec564920 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerExtensions.cs @@ -46,26 +46,14 @@ private static IServiceCollection WithDafnyWorkspace(this IServiceCollection ser serviceProvider.GetRequiredService>(), serviceProvider.GetRequiredService>()); }) - .AddSingleton(CreateTextDocumentLoader) + .AddSingleton() .AddSingleton() .AddSingleton(provider => (changes, cancellationToken) => new Migrator( provider.GetRequiredService>(), provider.GetRequiredService>(), changes, cancellationToken)) .AddSingleton() - .AddSingleton() .AddSingleton(); } - - public static TextDocumentLoader CreateTextDocumentLoader(IServiceProvider services) { - return TextDocumentLoader.Create( - services.GetRequiredService(), - services.GetRequiredService(), - services.GetRequiredService(), - services.GetRequiredService(), - services.GetRequiredService(), - services.GetRequiredService>() - ); - } } } diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index 9d894d58f77..e912ec3ed40 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -34,41 +34,82 @@ public async Task PublishNotifications(IdeState previousState, IdeState state) { return; } - PublishVerificationStatus(previousState, state); + PublishProgressStatus(previousState, state); PublishGhostness(previousState, state); await PublishDiagnostics(state); } - private void PublishVerificationStatus(IdeState previousState, IdeState state) { - var currentPerFile = GetFileVerificationStatus(state); - var previousPerFile = GetFileVerificationStatus(previousState); + private void PublishProgressStatus(IdeState previousState, IdeState state) { + foreach (var uri in state.Compilation.RootUris) { + // TODO, still have to check for ownedness - foreach (var (uri, current) in currentPerFile) { - if (previousPerFile.TryGetValue(uri, out var previous)) { - if (previous.NamedVerifiables.SequenceEqual(current.NamedVerifiables)) { - continue; - } + var current = GetProgressStatus(state, uri); + var previous = GetProgressStatus(previousState, uri); + + if (Equals(current, previous)) { + continue; + } + + switch (current) { + case ResolutionProgressStatus resolutionProgressStatus: + languageServer.SendNotification(new CompilationStatusParams { + Uri = uri, + Version = filesystem.GetVersion(uri), + Status = resolutionProgressStatus.CompilationStatus, + Message = null + }); + break; + case VerificationProgressStatus verificationProgressStatus: + languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, verificationProgressStatus.FileVerificationStatus); + break; + } + } + + } + + private abstract record ProgressStatus; + + private sealed record VerificationProgressStatus(FileVerificationStatus FileVerificationStatus) : ProgressStatus; + + private sealed record ResolutionProgressStatus(CompilationStatus CompilationStatus) : ProgressStatus; + + private ProgressStatus GetProgressStatus(IdeState state, Uri uri) { + var hasResolutionDiagnostics = (state.ResolutionDiagnostics.GetValueOrDefault(uri) ?? Enumerable.Empty()). + Any(d => d.Severity == DiagnosticSeverity.Error); + if (state.Compilation is CompilationAfterResolution) { + if (hasResolutionDiagnostics) { + return new ResolutionProgressStatus(CompilationStatus.ResolutionFailed); + } + + return new VerificationProgressStatus(GetFileVerificationStatus(state, uri)); + } + + if (state.Compilation is CompilationAfterParsing) { + if (hasResolutionDiagnostics) { + return new ResolutionProgressStatus(CompilationStatus.ParsingFailed); } - languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, current); + + return new ResolutionProgressStatus(CompilationStatus.ResolutionStarted); } + + return new ResolutionProgressStatus(CompilationStatus.Parsing); } - private static IDictionary GetFileVerificationStatus(IdeState state) { - return state.VerificationResults.GroupBy(kv => kv.Key.Uri). - ToDictionary(kv => kv.Key.ToUri(), kvs => - new FileVerificationStatus(kvs.Key, state.Compilation.Version, - kvs.Select(kv => GetNamedVerifiableStatuses(kv.Key, kv.Value)). - OrderBy(s => s.NameRange.Start).ToList())); + private FileVerificationStatus GetFileVerificationStatus(IdeState state, Uri uri) { + var verificationResults = state.GetVerificationResults(uri); + return new FileVerificationStatus(uri, filesystem.GetVersion(uri) ?? 0, + verificationResults.Select(kv => GetNamedVerifiableStatuses(kv.Key, kv.Value)). + OrderBy(s => s.NameRange.Start).ToList()); } - private static NamedVerifiableStatus GetNamedVerifiableStatuses(Location canVerify, IdeVerificationResult result) { + private static NamedVerifiableStatus GetNamedVerifiableStatuses(Range canVerify, IdeVerificationResult result) { var status = result.WasTranslated ? result.Implementations.Any() ? result.Implementations.Values.Select(v => v.Status).Aggregate(Combine) : PublishedVerificationStatus.Correct : PublishedVerificationStatus.Stale; - return new(canVerify.Range, status); + return new(canVerify, status); } static PublishedVerificationStatus Combine(PublishedVerificationStatus first, PublishedVerificationStatus second) { @@ -78,14 +119,12 @@ static PublishedVerificationStatus Combine(PublishedVerificationStatus first, Pu private readonly Dictionary> publishedDiagnostics = new(); private async Task PublishDiagnostics(IdeState state) { - var currentDiagnostics = state.GetDiagnostics(); - // All root uris are added because we may have to publish empty diagnostics for owned uris. - var sources = currentDiagnostics.Keys.Concat(state.Compilation.RootUris).Distinct(); + var sources = state.GetDiagnosticUris().Concat(state.Compilation.RootUris).Distinct(); var projectDiagnostics = new List(); foreach (var uri in sources) { - var current = currentDiagnostics.GetOrDefault(uri, Enumerable.Empty).ToArray(); + var current = state.GetDiagnosticsForUri(uri); var uriProject = await projectManagerDatabase.GetProject(uri); var ownedUri = uriProject.Equals(state.Compilation.Project); if (ownedUri) { @@ -94,7 +133,7 @@ private async Task PublishDiagnostics(IdeState state) { // since it also serves as a bucket for diagnostics from unowned files projectDiagnostics.AddRange(current); } else { - PublishForUri(uri, currentDiagnostics.GetOrDefault(uri, Enumerable.Empty).ToArray()); + PublishForUri(uri, current.ToArray()); } } else { var errors = current.Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); diff --git a/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs b/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs index 7fa121992a9..1940b2cf04f 100644 --- a/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs +++ b/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs @@ -10,8 +10,6 @@ public enum CompilationStatus { Parsing, ParsingFailed, ResolutionStarted, - ResolutionFailed, - CompilationSucceeded, // When resolution has succeeded - PreparingVerification, + ResolutionFailed } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index bd3f3982ae1..f5695afd73a 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -22,26 +22,23 @@ namespace Microsoft.Dafny.LanguageServer.Workspace { /// The increased stack size is necessary to solve the issue https://github.com/dafny-lang/dafny/issues/1447. /// public class TextDocumentLoader : ITextDocumentLoader { - private readonly ILogger documentLoader; + private readonly ILogger logger; private readonly IDafnyParser parser; private readonly ISymbolResolver symbolResolver; private readonly ISymbolTableFactory symbolTableFactory; private readonly IGhostStateDiagnosticCollector ghostStateDiagnosticCollector; - protected readonly ICompilationStatusNotificationPublisher statusPublisher; protected TextDocumentLoader( ILogger documentLoader, IDafnyParser parser, ISymbolResolver symbolResolver, ISymbolTableFactory symbolTableFactory, - IGhostStateDiagnosticCollector ghostStateDiagnosticCollector, - ICompilationStatusNotificationPublisher statusPublisher) { - this.documentLoader = documentLoader; + IGhostStateDiagnosticCollector ghostStateDiagnosticCollector) { + this.logger = documentLoader; this.parser = parser; this.symbolResolver = symbolResolver; this.symbolTableFactory = symbolTableFactory; this.ghostStateDiagnosticCollector = ghostStateDiagnosticCollector; - this.statusPublisher = statusPublisher; } public static TextDocumentLoader Create( @@ -49,10 +46,9 @@ public static TextDocumentLoader Create( ISymbolResolver symbolResolver, ISymbolTableFactory symbolTableFactory, IGhostStateDiagnosticCollector ghostStateDiagnosticCollector, - ICompilationStatusNotificationPublisher statusPublisher, ILogger logger ) { - return new TextDocumentLoader(logger, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector, statusPublisher); + return new TextDocumentLoader(logger, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector); } public IdeState CreateUnloaded(Compilation compilation) { @@ -73,15 +69,10 @@ private CompilationAfterParsing ParseInternal(DafnyOptions options, Compilation CancellationToken cancellationToken) { var project = compilation.Project; var errorReporter = new DiagnosticErrorReporter(options, project.Uri); - _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.Parsing); var program = parser.Parse(compilation, errorReporter, cancellationToken); var compilationAfterParsing = new CompilationAfterParsing(compilation, program, errorReporter.AllDiagnosticsCopy, compilation.RootUris.ToDictionary(uri => uri, uri => migratedVerificationTrees.GetValueOrDefault(uri) ?? new DocumentVerificationTree(program, uri))); - if (errorReporter.HasErrors) { - _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.ParsingFailed); - return compilationAfterParsing; - } return compilationAfterParsing; } @@ -108,18 +99,12 @@ private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compi var project = compilation.Project; - _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.ResolutionStarted); var compilationUnit = symbolResolver.ResolveSymbols(project, program, cancellationToken); var legacySymbolTable = symbolTableFactory.CreateFrom(compilationUnit, cancellationToken); var newSymbolTable = errorReporter.HasErrors ? null : symbolTableFactory.CreateFrom(program, compilation, cancellationToken); - if (errorReporter.HasErrors) { - _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.ResolutionFailed); - } else { - _ = statusPublisher.SendStatusNotification(compilation, CompilationStatus.CompilationSucceeded); - } var ghostDiagnostics = ghostStateDiagnosticCollector.GetGhostStateDiagnostics(legacySymbolTable, cancellationToken);