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

Flaky LSP test: DocumentAddedToExistingProjectDoesNotCrash #5434

Open
MikaelMayer opened this issue May 13, 2024 · 7 comments · Fixed by #5456
Open

Flaky LSP test: DocumentAddedToExistingProjectDoesNotCrash #5434

MikaelMayer opened this issue May 13, 2024 · 7 comments · Fixed by #5456
Assignees
@keyboardDrummer
Labels
kind: language development speed Slows down development of Dafny the language, flaky tests part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) priority: next Will consider working on this after in progress work is done

Comments

@MikaelMayer
Copy link
Member

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 MikaelMayer added part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) priority: next Will consider working on this after in progress work is done labels May 13, 2024
@MikaelMayer
Copy link
Member Author

Perhaps @keyboardDrummer ?

@keyboardDrummer keyboardDrummer self-assigned this May 14, 2024
@MikaelMayer MikaelMayer added the kind: language development speed Slows down development of Dafny the language, flaky tests label May 14, 2024
@MikaelMayer
Copy link
Member Author

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

@MikaelMayer
Copy link
Member Author

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

@MikaelMayer
Copy link
Member Author

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

@MikaelMayer
Copy link
Member Author

MikaelMayer commented May 16, 2024 •
edited
Loading

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 keyboardDrummer mentioned this issue May 17, 2024
Merged
keyboardDrummer added a commit that referenced this issue May 17, 2024
@keyboardDrummer
Attempt to fix the stability of DocumentAddedToExistingProjectDoesNot…
80583b7 
…Crash (#5456)

Fixes #5434

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
@keyboardDrummer
Copy link
Member

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

@keyboardDrummer
Copy link
Member

keyboardDrummer commented May 21, 2024 •
edited
Loading

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 #5447

keyboardDrummer added a commit to keyboardDrummer/dafny that referenced this issue May 21, 2024
@keyboardDrummer
Add log line to debug dafny-lang#5434
f982e5b
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@keyboardDrummer keyboardDrummer

Labels
kind: language development speed Slows down development of Dafny the language, flaky tests part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) priority: next Will consider working on this after in progress work is done
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Attempt to fix the stability of DocumentAddedToExistingProjectDoesNotCrash keyboardDrummer/dafny
2 participants
@keyboardDrummer @MikaelMayer