Flaky test failure: Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles.StandardLibrary.EditWhenUsingStandardLibrary

[robin-aws]

https://github.com/dafny-lang/dafny/actions/runs/8902097820/job/24447357000?pr=5383#step:10:233

[keyboardDrummer]

There should be a log line in the test log that comes from this line of code: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs#L61

But it's not there. Based on the stack trace I don't see how it could not be there.

Stack trace:

Failed Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles.StandardLibrary.EditWhenUsingStandardLibrary [48 s]
  Error Message:
   System.Threading.Tasks.TaskCanceledException : A task was canceled.
  Stack Trace:
     at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.WaitUntilResolutionFinished(TextDocumentItem documentId, CancellationToken cancellationToken) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs:line 207
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.WaitUntilAllStatusAreCompleted(TextDocumentItem documentId, Nullable`1 cancellationToken, Boolean allowStale) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs:line 179
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.GetLatestDiagnosticsParams(TextDocumentItem documentItem, CancellationToken cancellationToken, Boolean allowStale) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs:line 214
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.GetLastDiagnostics(TextDocumentItem documentItem, DiagnosticSeverity minimumSeverity, Nullable`1 cancellationToken, Boolean allowStale) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs:line 229
   at Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles.StandardLibrary.EditWhenUsingStandardLibrary() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/ProjectFiles/StandardLibrary.cs:line 25

The exception, TaskCanceledException, which inherits from OperationCanceledException, is thrown on this line:

compilationStatusParams = await compilationStatusReceiver.AwaitNextNotificationAsync(cancellationToken);

and that method contains:

public Task<TNotification> AwaitNextNotificationAsync(CancellationToken cancellationToken) {
  var start = DateTime.Now;
  try {
    return notifications.Dequeue(cancellationToken);
  } catch (OperationCanceledException) {
    var last = History.Any() ? History[^1].Stringify() : "none";
    logger.LogInformation($"Waited for {(DateTime.Now - start).Seconds} seconds for new notification.\n" +
                          $"Last received notification was {last}");
    throw;
  }

[keyboardDrummer]

Problem was that notifications.Dequeue(cancellationToken) is not awaited within the try/catch

[keyboardDrummer]

PR to help debug this issue the next time it occurs: https://github.com/dafny-lang/dafny/pull/5386

[keyboardDrummer]

For anyone who runs into this after the above PR is merged, please add your log link to this issue