Skip to content

Commit

Permalink
Fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed May 18, 2023
1 parent 36710d7 commit 4f4e095
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 10 deletions.
29 changes: 21 additions & 8 deletions Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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)]
Expand All @@ -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)]
Expand All @@ -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);
}

Expand Down
3 changes: 2 additions & 1 deletion Source/DafnyLanguageServer/Workspace/Compilation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,6 @@ private async Task<DocumentAfterTranslation> TranslateAsync() {
}

try {
statusPublisher.SendStatusNotification(resolvedCompilation.TextDocumentItem, CompilationStatus.PreparingVerification);
var translatedDocument = await PrepareVerificationTasksAsync(resolvedCompilation, cancellationSource.Token);
documentUpdates.OnNext(translatedDocument);
foreach (var task in translatedDocument.VerificationTasks!) {
Expand All @@ -134,6 +133,8 @@ public async Task<DocumentAfterTranslation> PrepareVerificationTasksAsync(
throw new TaskCanceledException();
}

statusPublisher.SendStatusNotification(loaded.TextDocumentItem, CompilationStatus.PreparingVerification);

var verificationTasks =
await verifier.GetVerificationTasksAsync(loaded, cancellationToken);

Expand Down
1 change: 0 additions & 1 deletion Source/DafnyLanguageServer/Workspace/DafnyDocument.cs
View file

This file was deleted.

0 comments on commit 4f4e095

Please sign in to comment.