From db1b5a2e2df92ce2a2310171a9a3146207e43684 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 14:37:31 +0200 Subject: [PATCH 1/2] Draft of moving compilation status updates to the notification publisher --- .../DeclarationLocationMigrationTest.cs | 2 +- .../Synchronization/IncludeFileTest.cs | 2 +- .../Synchronization/LookupMigrationTest.cs | 2 +- .../Synchronization/OpenDocumentTest.cs | 25 +++--- .../Unit/CompilationManagerTest.cs | 2 - .../Unit/TextDocumentLoaderTest.cs | 5 -- .../Util/ClientBasedLanguageServerTest.cs | 3 +- .../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 | 89 ++++++++++++++----- .../Workspace/TextDocumentLoader.cs | 23 +---- 21 files changed, 161 insertions(+), 171 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..7216df87387 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.GetDiagnosticUris()); } // 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/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..059fb914f4e 100644 --- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs +++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs @@ -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/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..b1484c06acb 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -34,41 +34,86 @@ 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; } - languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, current); } + } - 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 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); + } + + var verificationResults = state.GetVerificationResults(uri); + if (verificationResults.Any()) { + return new VerificationProgressStatus(GetFileVerificationStatus(state, uri)); + } + return new ResolutionProgressStatus(CompilationStatus.CompilationSucceeded); + } + + if (state.Compilation is CompilationAfterParsing) { + if (hasResolutionDiagnostics) { + return new ResolutionProgressStatus(CompilationStatus.ParsingFailed); + } + + return new ResolutionProgressStatus(CompilationStatus.ResolutionStarted); + } + + return new ResolutionProgressStatus(CompilationStatus.Parsing); } - private static NamedVerifiableStatus GetNamedVerifiableStatuses(Location canVerify, IdeVerificationResult result) { + 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(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 +123,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 +137,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/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); From 49bb4e1ac115596e6a984209c4a507d9ca9d8ee8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Aug 2023 15:20:51 +0200 Subject: [PATCH 2/2] Fix test --- .../Synchronization/IncludeFileTest.cs | 2 +- .../Synchronization/VerificationStatusTest.cs | 2 + .../Util/ClientBasedLanguageServerTest.cs | 4 +- .../CompilationStatusNotificationTest.cs | 37 +++++++------------ .../Workspace/NotificationPublisher.cs | 6 +-- .../Notifications/CompilationStatus.cs | 4 +- 6 files changed, 20 insertions(+), 35 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs index 7216df87387..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.Empty(document.GetDiagnosticUris()); + Assert.Empty(document.GetAllDiagnostics()); } // https://github.com/dafny-lang/language-server-csharp/issues/40 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/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs index 059fb914f4e..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); 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/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index b1484c06acb..e912ec3ed40 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -81,11 +81,7 @@ private ProgressStatus GetProgressStatus(IdeState state, Uri uri) { return new ResolutionProgressStatus(CompilationStatus.ResolutionFailed); } - var verificationResults = state.GetVerificationResults(uri); - if (verificationResults.Any()) { - return new VerificationProgressStatus(GetFileVerificationStatus(state, uri)); - } - return new ResolutionProgressStatus(CompilationStatus.CompilationSucceeded); + return new VerificationProgressStatus(GetFileVerificationStatus(state, uri)); } if (state.Compilation is CompilationAfterParsing) { 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 } }