Remy Willems

Deduplicate verification diagnostic reporting between CLI and server

2

### Description Mature the `IPhase` concept by bigger use of it in more locations. In particular, it is now used for verification and verification coverage diagnostics. Specific changes: - Let...

Do not allow building libraries while silently not verifing included files

3

Fixes #4762 (actually, it's only truly fixed until we remove `--verify-included files`, but our migration policy prevents doing this until we do another release. IMO the migration policy of always...

Add `dafny migrate` to support migration and reduce backwards compatibility requirements

1

Currently [this](https://github.com/dafny-lang/dafny/blob/master/CONTRIBUTING.md#backwards-compatibility) document that contains guidelines for the development of Dafny, reads `As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they...

https://github.com/dafny-lang/dafny/actions/runs/8982278222/job/24669541310?pr=5397 ``` [xUnit.net 00:04:02.88] --- End of stack trace from previous location --- Failed Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles.CompetingProjectFilesTest.ProjectFileDoesNotOwnAllSourceFilesItUses [49 s] Error Message: System.Threading.Tasks.TaskCanceledException : A task was canceled. Stack Trace: at Microsoft.Dafny.LanguageServer.IntegrationTest.Util.TestNotificationReceiver`1.AwaitNextNotificationAsync(CancellationToken cancellationToken)...

Unstable test: System.NullReferenceException at Microsoft.Boogie.ReadOnlyVisitor.VisitVariable

3

Run: https://github.com/dafny-lang/dafny/actions/runs/5760643103/job/15617339950?pr=4357 ``` [xUnit.net 00:19:12.55] Finished: IntegrationTests Failed VSI-Benchmarks/b6.dfy [14 s] Error Message: System.Exception : Command returned non-zero exit code (134): dotnet /home/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/Dafny.dll /vcsCores:2 /useBaseNameForFileName /compileVerbose:0 /timeLimit:300 /showSnippets:0 /compile:0 TestFiles/LitTests/LitTest/VSI-Benchmarks/b6.dfy...

Enable safely using doo files that were verified against other doo files

4

If I have project A, A*, B and C, where B depends on A, C depends on B, and A and A* have the same type signature. Then if I...

Unstable counterexample test

2

The test `DatatypeObjectWithTwoDestructorsWhoseValuesAreEqual` seems to fail sometimes. https://github.com/dafny-lang/dafny/actions/runs/5998742793/job/16268642812?pr=4476 ``` [xUnit.net 00:00:45.61] --- End of stack trace from previous location --- Failed Microsoft.Dafny.LanguageServer.IntegrationTest.Various.CounterExampleTest.DatatypeObjectWithTwoDestructorsWhoseValuesAreEqual(optionSettings: Action`1 { Method = Void b__1_0(Microsoft.Dafny.DafnyOptions), Target =...

Unstable test NoExtraThreadAfterEachChange

1

https://github.com/dafny-lang/dafny/actions/runs/8909099093/job/24465880216?pr=5359 ``` [xUnit.net 00:12:47.72] --- End of stack trace from previous location --- Failed Microsoft.Dafny.LanguageServer.IntegrationTest.Performance.ThreadUsageTest.NoExtraThreadAfterEachChange [11 s] Error Message: Assert.InRange() Failure Range: (-5 - 5) Actual: -9 Stack Trace: at...

Unstable VerificationErrorDetectedAfterCanceledSave

1

https://github.com/dafny-lang/dafny/actions/runs/8520037939/job/23335354897?pr=5284 There was a concurrent collection modification exception, but sadly only part of the exception is shown in the log: ``` [xUnit.net 00:03:27.83] --- End of stack trace from previous...

Unstable test QuickEditsInLargeFile

1

https://github.com/dafny-lang/dafny/actions/runs/8571621530/job/23492819569?pr=5301 ``` [xUnit.net 00:09:30.53] lowest division 0.7067082821128992 Failed Microsoft.Dafny.LanguageServer.IntegrationTest.Performance.LargeFilesTest.QuickEditsInLargeFile [2 m 6 s] Error Message: averageTimeToSchedule: 129.15138775510204 Expected: True Actual: False Stack Trace: at Microsoft.Dafny.LanguageServer.IntegrationTest.Performance.LargeFilesTest.QuickEditsInLargeFile() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs:line 92 --- End...