search

dafny-lang / dafny

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

Flaky LSP test: DocumentAddedToExistingProjectDoesNotCrash #5434

Open MikaelMayer opened 6 months ago

MikaelMayer commented 6 months ago

Seen here: https://github.com/dafny-lang/dafny/actions/runs/9070337566/job/24922923041?pr=5433

Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.CachingTest.DocumentAddedToExistingProjectDoesNotCrash [FAIL]
[xUnit.net 00:00:18.30]       diagnostics[1,1,0,0]: Diagnostic { Range = [start: (3, 12), end: (3, 14)], Severity = Error, Code = OmniSharp.Extensions.LanguageServer.Protocol.Models.DiagnosticCode, CodeDescription = CodeDescription { Href = https://dafny.org/dafny/HowToFAQ/Errors#none }, Source = Resolver, Message = RHS (of type bool) not assignable to LHS (of type int), Tags = , RelatedInformation = OmniSharp.Extensions.LanguageServer.Protocol.Models.Container`1[OmniSharp.Extensions.LanguageServer.Protocol.Models.DiagnosticRelatedInformation], Data =  }
[xUnit.net 00:00:18.30]       Stack Trace:
[xUnit.net 00:00:18.30]            at XunitAssertMessages.AssertM.WithMessage(String message, Action action)
[xUnit.net 00:00:18.30]            at XunitAssertMessages.AssertM.Equal[T](T expected, T actual, String userMessage)
[xUnit.net 00:00:18.30]         D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Synchronization\CachingTest.cs(380,0): at Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.CachingTest.DocumentAddedToExistingProjectDoesNotCrash()
MikaelMayer commented 6 months ago

Perhaps @keyboardDrummer ?

MikaelMayer commented 6 months ago

Hit that one again today https://github.com/dafny-lang/dafny/actions/runs/9098687342/job/25011441051?pr=5441

MikaelMayer commented 6 months ago

Got it again here: https://github.com/dafny-lang/dafny/actions/runs/9114303510/job/25059195114?pr=5441

MikaelMayer commented 6 months ago

Hit this issue again here https://github.com/dafny-lang/dafny/actions/runs/9114307966/job/25059377435?pr=5440

MikaelMayer commented 6 months ago

And here as well

https://github.com/dafny-lang/dafny/actions/runs/9116216246/job/25064347648?pr=5442 https://github.com/dafny-lang/dafny/actions/runs/9116216246/job/25064347423?pr=5442

keyboardDrummer commented 6 months ago

Not fixed: https://github.com/dafny-lang/dafny/actions/runs/9115852973/job/25063146075?pr=5447

keyboardDrummer commented 6 months ago

Somehow in the final compilation, one of the sources is not considered owned by the project, so its errors are reported as "out of project" diagnostics on the project file. Caching on determining the project file of a file is turned off, and determinedRootFiles.Roots must contain the not owned file because diagnostics coming from the file are reported by the project.

Adding extra logging in https://github.com/dafny-lang/dafny/pull/5447

MikaelMayer commented 1 day ago

Hit again https://github.com/dafny-lang/dafny/actions/runs/12032701079/job/33545154044?pr=5933: Here is the log

info: default[0]
      Waited for 49 seconds for new notification.
      Last received notification was CompilationStatusParams {
        Uri = file:///tmp/gfmru11l.5jz/source1.dfy,
        Version = 1,
        Status = ResolutionFailed
      }
[xUnit.net 00:03:14.65]     Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization.CachingTest.DocumentAddedToExistingProjectDoesNotCrash [FAIL]
[xUnit.net 00:03:14.65]       System.Threading.Tasks.TaskCanceledException : A task was canceled.
[xUnit.net 00:03:14.65]       Stack Trace:
[xUnit.net 00:03:14.66]         /home/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs(58,0): at