search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

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

Open RustanLeino opened 2 weeks ago

RustanLeino commented 2 weeks ago

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 commented 2 weeks ago

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 commented 2 weeks ago

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

keyboardDrummer commented 2 weeks ago

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.