search

dafny-lang / dafny

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

Testing: assert that the language server behaves equivalently to the CLI #1547

Open robin-aws opened 2 years ago

robin-aws commented 2 years ago

More follow-up from #1426 and in particular #1430.

To help avoid future instances of an IDE giving information that contradicts the CLI, we can create a testing utility that prints the results of requests to the language server in the same format as the CLI, and then asserting that the matches the CLI's output on various input programs.

keyboardDrummer commented 2 years ago

Can you specify in the ticket what information you'd like to compare? I expect the language server to provide a lot of information that the Dafny CLI does not. The information that I think can be compared are diagnostics, and whether the server/CLI returns or hangs/crashes.

Would a different way of specifying this ticket be to say you want to test the language server against the Dafny programs in Dafny's regression suite?

For the implementation, consider transforming the Dafny CLI output to the same format as the language server, since that's a standardised format (LSP). Also, for a program that correctly verifies, the CLI can provide information that the IDE can not, such as the stdout output of running the program. Converting the CLI output to LSP diagnostics (an empty list) is thus possible, but not the other way around.