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

Move compilation status updates to notification publisher #4454

Merged
merged 2 commits into from
Aug 23, 2023
Merged

Move compilation status updates to notification publisher #4454

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
db1b5a2
Draft of moving compilation status updates to the notification publisher
keyboardDrummer Aug 23, 2023
49bb4e1
Fix test
keyboardDrummer Aug 23, 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
2 changes: 1 addition & 1 deletion Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyLanguageServer.Test/Synchronization/LookupMigrationTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
25 changes: 12 additions & 13 deletions Source/DafnyLanguageServer.Test/Synchronization/OpenDocumentTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ public Task DisposeAsync() {
}

private async Task SetUp(Action<DafnyOptions> modifyOptions) {
(client, Server) = await Initialize(options => { }, modifyOptions);
(client, Server) = await Initialize(_ => { }, modifyOptions);
}

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

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

Expand Down Expand Up @@ -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]
Expand All @@ -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]
Expand All @@ -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]
Expand All @@ -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) {
Expand Down
2 changes: 2 additions & 0 deletions Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down
2 changes: 0 additions & 2 deletions Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,7 @@ public async Task CancelUnstartedCompilationLeadsToCancelledTasks() {
var dafnyOptions = DafnyOptions.Create(TextWriter.Null, TextReader.Null);
var compilationManager = new CompilationManager(new Mock<ILogger<CompilationManager>>().Object,
new Mock<ITextDocumentLoader>().Object,
new Mock<INotificationPublisher>().Object,
new Mock<IProgramVerifier>().Object,
new Mock<ICompilationStatusNotificationPublisher>().Object,
new Mock<IVerificationProgressReporter>().Object,
dafnyOptions,
null, new Compilation(0, new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }, new Uri[] { }), null);
Expand Down
5 changes: 0 additions & 5 deletions Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,27 +23,22 @@ public class TextDocumentLoaderTest {
private Mock<ISymbolResolver> symbolResolver;
private Mock<ISymbolTableFactory> symbolTableFactory;
private Mock<IGhostStateDiagnosticCollector> ghostStateDiagnosticCollector;
private Mock<ICompilationStatusNotificationPublisher> notificationPublisher;
private TextDocumentLoader textDocumentLoader;
private Mock<ILogger<ITextDocumentLoader>> logger;
private Mock<INotificationPublisher> diagnosticPublisher;

public TextDocumentLoaderTest(ITestOutputHelper output) {
this.output = new WriterFromOutputHelper(output);
parser = new();
symbolResolver = new();
symbolTableFactory = new();
ghostStateDiagnosticCollector = new();
notificationPublisher = new();
fileSystem = new();
logger = new Mock<ILogger<ITextDocumentLoader>>();
diagnosticPublisher = new Mock<INotificationPublisher>();
textDocumentLoader = TextDocumentLoader.Create(
parser.Object,
symbolResolver.Object,
symbolTableFactory.Object,
ghostStateDiagnosticCollector.Object,
notificationPublisher.Object,
logger.Object
);
}
Expand Down
7 changes: 3 additions & 4 deletions Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,12 +94,12 @@ private void AssertMatchRegex(string expected, string value) {
}
}

public async Task<NamedVerifiableStatus> WaitForStatus(Range nameRange, PublishedVerificationStatus statusToFind,
public async Task<NamedVerifiableStatus> 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);
Expand Down Expand Up @@ -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<Diagnostic>.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())));
Expand Down
37 changes: 13 additions & 24 deletions Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why did you remove the ensures clause?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Part of debugging, but it's not needed

return 2;
}".TrimStart();
var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
Expand All @@ -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) {
Expand All @@ -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)]
Expand All @@ -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);
}

Expand All @@ -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);
}
Expand All @@ -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);
Expand All @@ -132,28 +129,25 @@ 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)]
public async Task DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() {
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)]
Expand All @@ -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)]
Expand All @@ -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)]
Expand All @@ -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);
}

Expand Down
Loading
Loading