search

dafny-lang / dafny

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

Unstable test 'VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions #5319

Open keyboardDrummer opened 3 months ago

keyboardDrummer commented 3 months ago

https://github.com/dafny-lang/dafny/actions/runs/8661038066/job/23750160791?pr=5318

xUnit.net 00:14:41.69]     Microsoft.Dafny.LanguageServer.IntegrationTest.Various.DiagnosticMigrationTest.VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions [FAIL]
[xUnit.net 00:14:41.70]       Assert.Empty() Failure
[xUnit.net 00:14:41.70]       Expected: <empty>
[xUnit.net 00:14:41.70]       Actual:   [Diagnostic { Range = [start: (4, 4), end: (4, 10)], Severity = Warning, Code = OmniSharp.Extensions.LanguageServer.Protocol.Models.DiagnosticCode, CodeDescription = , Source = Verifier, Message = Outdated: a postcondition could not be proved on this return path, Tags = , RelatedInformation = OmniSharp.Extensions.LanguageServer.Protocol.Models.Container`1[OmniSharp.Extensions.LanguageServer.Protocol.Models.DiagnosticRelatedInformation], Data =  }]
[xUnit.net 00:14:41.70]       Stack Trace:
[xUnit.net 00:14:41.70]         /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs(144,0): at Microsoft.Dafny.LanguageServer.IntegrationTest.Various.DiagnosticMigrationTest.VerificationDiagnosticsCanBeMigratedAcrossMultipleResolutions()
[xUnit.net 00:14:41.70]         --- End of stack trace from previous location ---
keyboardDrummer commented 2 months ago

Given recent server improvements it's unclear whether this still exists. Keeping open for a few weeks to see if it reoccurs.