From 4f4e095ab58d996b94dd9971bf62a6a2fcf47486 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 18 May 2023 12:11:58 +0200 Subject: [PATCH] Fix tests --- .../CompilationStatusNotificationTest.cs | 29 ++++++++++++++----- .../Workspace/Compilation.cs | 3 +- .../Workspace/DafnyDocument.cs | 1 - 3 files changed, 23 insertions(+), 10 deletions(-) delete mode 100644 Source/DafnyLanguageServer/Workspace/DafnyDocument.cs diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index e451437e480..39a216cc1f7 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -46,13 +46,13 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); + 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.ResolutionStarted); + await AssertProgress(otherDoc, CompilationStatus.Parsing); await AssertProgress(otherDoc, CompilationStatus.ParsingFailed); } @@ -67,12 +67,14 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source); 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); } @@ -91,6 +93,7 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); } @@ -115,6 +118,7 @@ method Abs(x: int) returns (y: int) ".TrimStart(); var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); } @@ -123,6 +127,7 @@ method Abs(x: int) returns (y: int) public async Task DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() { var documentItem = CreateTestDocument(SlowToVerify); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); } @@ -132,6 +137,7 @@ public async Task DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucce await SetUp(options => options.Set(BoogieOptionBag.VerificationTimeLimit, 3U)); var documentItem = CreateTestDocument(SlowToVerify); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded); } @@ -151,13 +157,16 @@ 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); - var documentItem2 = CreateTestDocument(source, "test_2dfy"); - await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken); - + await AssertProgress(documentItem1, CompilationStatus.Parsing); await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded); + await AssertProgress(documentItem1, CompilationStatus.PreparingVerification); + 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 AssertProgress(documentItem2, CompilationStatus.PreparingVerification); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -176,13 +185,17 @@ 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 AssertProgress(documentItem1, CompilationStatus.PreparingVerification); var documentItem2 = CreateTestDocument(source, "test_2dfy"); await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken); await client.SaveDocumentAndWaitAsync(documentItem2, CancellationToken); - await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted); - await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded); + await AssertProgress(documentItem2, CompilationStatus.Parsing); await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted); await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded); + await AssertProgress(documentItem2, CompilationStatus.PreparingVerification); } [Fact(Timeout = MaxTestExecutionTimeMs)] @@ -196,7 +209,7 @@ lemma Something(i: int) }"; var documentItem = CreateTestDocument(source); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); - await AssertProgress(documentItem, CompilationStatus.ResolutionStarted); + await AssertProgress(documentItem, CompilationStatus.Parsing); await AssertProgress(documentItem, CompilationStatus.ParsingFailed); } diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs index df3cd01cb2a..42194d64e95 100644 --- a/Source/DafnyLanguageServer/Workspace/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs @@ -110,7 +110,6 @@ private async Task TranslateAsync() { } try { - statusPublisher.SendStatusNotification(resolvedCompilation.TextDocumentItem, CompilationStatus.PreparingVerification); var translatedDocument = await PrepareVerificationTasksAsync(resolvedCompilation, cancellationSource.Token); documentUpdates.OnNext(translatedDocument); foreach (var task in translatedDocument.VerificationTasks!) { @@ -134,6 +133,8 @@ public async Task PrepareVerificationTasksAsync( throw new TaskCanceledException(); } + statusPublisher.SendStatusNotification(loaded.TextDocumentItem, CompilationStatus.PreparingVerification); + var verificationTasks = await verifier.GetVerificationTasksAsync(loaded, cancellationToken); diff --git a/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs b/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs deleted file mode 100644 index 5f282702bb0..00000000000 --- a/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs +++ /dev/null @@ -1 +0,0 @@ - \ No newline at end of file