Test suite fails on LanguageServer.IntegrationTest.Synchronization.DiagnosticsTest.OpeningDocumentWithMultipleVerificationCoresReturnsStableDiagnostics

[RustanLeino]

Dafny version

master branch, 2 Nov 2024

Code to produce this issue

Lately, I've observed this error several times. It seems to occur only on the xunit-tests/win job.

The exception stack trace is shown below. I don't know if the following link will persist, but at the moment it shows the error:
https://github.com/dafny-lang/dafny/actions/runs/11655717078/job/32450782693?pr=5891

Command to run and resulting output

...
[xUnit.net 00:04:54.18]         D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Diagnostics\DiagnosticsTest.cs(927,0): at Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.DiagnosticsTest.OpeningDocumentWithMultipleVerificationCoresReturnsStableDiagnostics()
[xUnit.net 00:04:54.18]         --- End of stack trace from previous location ---
  Failed Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.DiagnosticsTest.OpeningDocumentWithMultipleVerificationCoresReturnsStableDiagnostics [50 s]
  Error Message:
   System.Threading.Tasks.TaskCanceledException : A task was canceled.
  Stack Trace:
     at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.TestNotificationReceiver`1.AwaitNextNotificationAsync(CancellationToken cancellationToken) in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Util\TestNotificationReceiver.cs:line 58
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.WaitUntilAllStatusAreCompleted(TextDocumentItem documentId, Nullable`1 cancellationToken, Boolean allowStale) in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Util\ClientBasedLanguageServerTest.cs:line 188
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.GetLatestDiagnosticsParams(TextDocumentItem documentItem, CancellationToken cancellationToken, Boolean allowStale) in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Util\ClientBasedLanguageServerTest.cs:line 219
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.ClientBasedLanguageServerTest.GetLastDiagnostics(TextDocumentItem documentItem, DiagnosticSeverity minimumSeverity, Nullable`1 cancellationToken, Boolean allowStale) in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Util\ClientBasedLanguageServerTest.cs:line 234
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.DiagnosticsTest.OpeningDocumentWithMultipleVerificationCoresReturnsStableDiagnostics() in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Diagnostics\DiagnosticsTest.cs:line 927
--- End of stack trace from previous location ---
  Passed Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.DiagnosticsTest.OpeningDocumentWithVerificationErrorReportsDiagnosticsWithVerificationErrors [208 ms]
      Opening file file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
      Migrated LastPublishedState to version 1, uri file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyTextDocumentHandler[0]
      Finished opening document file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Language.CachingParser[0]
      Parse cache miss for file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.ProjectManager[0]
      HandleDeterminedRootFiles found project for file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy to be file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
      Updated LastPublishedState to version 1, uri file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Language.CachingParser[0]
      encountered 1 errors while parsing file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
      Updated LastPublishedState to version 1, uri file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.Compilation[0]
      Passed parsedCompilation to documentUpdates.OnNext, resolving ParsedCompilation task for version 1.
trce: Microsoft.Dafny.LanguageServer.Workspace.NotificationPublisher[0]
      Publish diagnostics called for URI file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.IdeStateObserver[0]
      Updated LastPublishedState to version 1, uri file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler[0]
      received hover request for file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.ProjectManagerDatabase[0]
      project manager found for file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Handlers.DafnyTextDocumentHandler[0]
      received close notification file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
dbug: Microsoft.Dafny.LanguageServer.Workspace.LanguageServerFilesystem[0]
      Closing document file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
trce: Microsoft.Dafny.LanguageServer.Workspace.NotificationPublisher[0]
      Publish diagnostics called for URI file:///c:/Users/runneradmin/AppData/Local/Temp/vlntrw2c.dsb/AssertNoDiagnosticsAreComing146.dfy
  Passed Microsoft.Dafny.LanguageServer.IntegrationTest.Unit.TextReaderFromCharArraysTest.ReadPeekEmptyStart [< 1 ms]
  Passed Microsoft.Dafny.LanguageServer.IntegrationTest.Unit.TextReaderFromCharArraysTest.ReadMoreThanContent [1 ms]
...

What happened?

CI on github fails. The error only happens sometimes, so I will probably be able to work around it by re-running the CI job.

What type of operating system are you experiencing the problem on?

Windows

[keyboardDrummer]

Since this only/mostly occurs on Windows machines, this might just be an honest timeout, where the Windows machines is slower and that's why the test has a chance of timing out. Next step is to check how long the test takes on Windows machines when it does pass, and possibly incrementing the timeout value or reducing the amount of work

[RustanLeino]

What is setting that time out? Why is a time out set on the CI test suite?

[keyboardDrummer]

Why is a time out set on the CI test suite?

That's standard for any automated test, so that when you make a mistake the CI does not go on endlessly

What is setting that time out?

The default timeout is 50 seconds. Configured here: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs#L63
new JsonRpcTestOptions has a CancellationTimeout property whose default value is 50seconds.