Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add additional IDE status messages #4031

Merged
merged 5 commits into from
May 18, 2023
Merged

Add additional IDE status messages #4031

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
b880b18
Add additional IDE status messages, so users aren't wondering what ha…
keyboardDrummer May 16, 2023
b3c2e3e
Add release note
keyboardDrummer May 17, 2023
36710d7
Merge branch 'master' into extraStates
keyboardDrummer May 17, 2023
4f4e095
Fix tests
keyboardDrummer May 18, 2023
25f612a
Merge branch 'master' into extraStates
keyboardDrummer May 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 21 additions & 8 deletions Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
View file
Open in desktop
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
2 changes: 2 additions & 0 deletions Source/DafnyLanguageServer/Workspace/Compilation.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,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
Open in desktop

This file was deleted.

4 changes: 3 additions & 1 deletion Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@ namespace Microsoft.Dafny.LanguageServer.Workspace.Notifications {
/// </summary>
[JsonConverter(typeof(StringEnumConverter))]
public enum CompilationStatus {
ResolutionStarted,
Parsing,
ParsingFailed,
ResolutionStarted,
ResolutionFailed,
PreparingVerification,
CompilationSucceeded
}
}
3 changes: 2 additions & 1 deletion Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,14 +84,15 @@ private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuff
CancellationToken cancellationToken) {
var outerModule = new DefaultModuleDefinition(new List<Uri>() { textDocument.Uri.ToUri() });
var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri);
statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted);
statusPublisher.SendStatusNotification(textDocument, CompilationStatus.Parsing);
var program = parser.Parse(textDocument, errorReporter, cancellationToken);
var documentAfterParsing = new DocumentAfterParsing(textDocument, program, errorReporter.GetDiagnostics(textDocument.Uri));
if (errorReporter.HasErrors) {
statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ParsingFailed);
return documentAfterParsing;
}

statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted);
var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, out _, cancellationToken);
var symbolTable = symbolTableFactory.CreateFrom(compilationUnit, cancellationToken);

Expand Down
1 change: 1 addition & 0 deletions docs/dev/news/4031.feat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Allow the Dafny IDE to publish 'Parsing' and 'Preparing Verification' messages to let the user better understand what they're waiting for.